Theorem r19.42v 3350

Description: Restricted quantifier version of 19.42v 1954 (see also 19.42 2238). (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 3347	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 463	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3247	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 463	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 305	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-rex 3144

This theorem is referenced by:  rexcom  3355  ceqsrexbv  3642  ceqsrex2v  3643  2reuswap  3728  2reuswap2  3729  2reu5  3740  2rmoswap  3743  iunrab  4962  iunin2  4979  iundif2  4982  reusv2lem4  5288  iunopab  5432  cnvuni  5743  elidinxp  5897  xpdifid  6011  elunirn  6996  f1oiso  7090  oprabrexex2  7665  oeeu  8215  trcl  9156  dfac5lem2  9536  axgroth4  10240  rexuz2  12286  4fvwrd4  13017  cshwsexa  14171  divalglem10  15736  divalgb  15738  lsmelval2  19840  tgcmp  21992  hauscmplem  21997  unisngl  22118  xkobval  22177  txtube  22231  txcmplem1  22232  txkgen  22243  xkococnlem  22250  mbfaddlem  24244  mbfsup  24248  elaa  24891  dchrisumlem3  26053  colperpexlem3  26504  midex  26509  iscgra1  26582  ax5seg  26710  edglnl  26914  usgr2pth0  27532  hhcmpl  28961  sumdmdii  30176  reuxfrdf  30239  unipreima  30377  fpwrelmapffslem  30454  esumfsup  31336  reprdifc  31905  bnj168  32007  bnj1398  32313  cvmliftlem15  32552  dfpo2  32998  ellines  33620  bj-elsngl  34296  bj-dfmpoa  34426  ptrecube  34926  cnambfre  34974  islshpat  36185  lfl1dim  36289  glbconxN  36546  3dim0  36625  2dim  36638  1dimN  36639  islpln5  36703  islvol5  36747  dalem20  36861  lhpex2leN  37181  mapdval4N  38800  rexrabdioph  39483  rmxdioph  39705  expdiophlem1  39710  imaiun1  40086  coiun1  40087  ismnuprim  40720  prmunb2  40733  fourierdlem48  42529  2reuimp0  43403  2reuimp  43404  wtgoldbnnsum4prm  44052  bgoldbnnsum3prm  44054  islindeps2  44623  isldepslvec2  44625