Theorem 19.42v 1983

Description: Version of 19.42 2272 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
19.42v	⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		19.41v 1979	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1891	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 465	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 306	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400  ∃wex 1809

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is used by:  exdistr  1984  19.42vv  1987  19.42vvv  1989  4exdistr  1991  2sb5  2313  eeeanv  2382  eu6lem  2601  r3ex  3204  rexcom4a  3295  ceqsex2  3505  ceqsex2v  3506  reuind  3716  2reu5lem3  3720  sbccomlemOLD  3823  bm1.3iiOLD  5265  eqvinop  5469  copsexgw  5472  dfid2  5558  dmopabss  5908  dmopab3  5909  dmxp  5919  rnopabss  5945  rnopab3  5946  dmres  6011  ssrnres  6176  mptpreima  6239  resco  6251  mptfnf  6670  brprcneu  6871  brprcneuALT  6872  fndmin  7040  fliftf  7313  dfoprab2  7468  dmoprab  7513  dmoprabss  7514  fnoprabg  7533  uniuni  7757  zfrep6OLD  7948  opabex3d  7958  opabex3rd  7959  opabex3  7960  fsplit  8108  eroveu  8806  ensymfib  9164  rankuni  9831  aceq1  10106  dfac3  10110  kmlem14  10152  kmlem15  10153  axdc2lem  10436  1idpr  11018  ltexprlem1  11025  ltexprlem4  11028  xpcogend  15016  shftdm  15113  joindm  18433  meetdm  18447  toprntopon  23091  ntreq0  23243  cnextf  24232  dmcuts  27993  adjeu  32250  rexunirn  32847  fpwrelmapffslem  33086  mxidlnzrb  33771  tgoldbachgt  35059  bnj1019  35177  bnj1209  35193  bnj1033  35366  bnj1189  35406  karddom  35582  kardsdom  35583  vonf1oonfo  35607  satfdm  35869  dfiota3  36421  brimg  36435  funpartlem  36442  bj-eeanvw  37368  bj-snsetex  37627  bj-snglc  37633  bj-bm1.3ii  37728  bj-dfid2ALT  37729  bj-axreprepsep  37740  bj-restuni  37767  bj-xpcossxp  37861  bj-imdirco  37862  itg2addnc  38353  sbccom2lem  38801  eldmres  38954  rnxrn  39098  coss1cnvres  39184  nnoeomeqom  44067  rp-isfinite6  44272  undmrnresiss  44358  elintima  44407  pm11.58  45128  pm11.71  45135  2sbc5g  45154  iotasbc2  45158  ax6e2nd  45295  ax6e2ndVD  45644  ax6e2ndALT  45666  modelaxreplem3  45717  stoweidlem60  46802  coxp  49639  mofeu  49654  uobffth  50024  uobeqw  50025  elpglem3  50519