Theorem r19.42v 3092

Description: Restricted quantifier version of 19.42v 1918 (see also 19.42 2105). (Contributed by NM, 27-May-1998.)

Assertion

Ref	Expression
r19.42v	⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.42v

Step	Hyp	Ref	Expression
1		r19.41v 3089	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 466	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3041	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 466	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 292	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 384  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-rex 2918

This theorem is referenced by:  ceqsrexbv  3337  ceqsrex2v  3338  2reuswap  3410  2reu5  3416  iunrab  4567  iunin2  4584  iundif2  4587  reusv2lem4  4872  iunopab  5012  elxp2OLD  5133  cnvuni  5309  xpdifid  5562  elunirn  6509  f1oiso  6601  oprabrexex2  7158  oeeu  7683  trcl  8604  dfac5lem2  8947  axgroth4  9654  rexuz2  11739  4fvwrd4  12459  cshwsexa  13570  divalglem10  15125  divalgb  15127  lsmelval2  19085  tgcmp  21204  hauscmplem  21209  unisngl  21330  xkobval  21389  txtube  21443  txcmplem1  21444  txkgen  21455  xkococnlem  21462  mbfaddlem  23427  mbfsup  23431  elaa  24071  dchrisumlem3  25180  colperpexlem3  25624  midex  25629  iscgra1  25702  ax5seg  25818  edglnl  26038  usgr2pth0  26661  sumdmdii  29274  2reuswap2  29328  unipreima  29446  fpwrelmapffslem  29507  esumfsup  30132  reprdifc  30705  bnj168  30798  bnj1398  31102  cvmliftlem15  31280  dfpo2  31645  ellines  32259  bj-elsngl  32956  bj-dfmpt2a  33071  ptrecube  33409  cnambfre  33458  islshpat  34304  lfl1dim  34408  glbconxN  34664  3dim0  34743  2dim  34756  1dimN  34757  islpln5  34821  islvol5  34865  dalem20  34979  lhpex2leN  35299  mapdval4N  36921  rexrabdioph  37358  rmxdioph  37583  expdiophlem1  37588  imaiun1  37943  coiun1  37944  prmunb2  38510  fourierdlem48  40371  2rmoswap  41184  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  islindeps2  42272  isldepslvec2  42274