Theorem 19.42v 1987

Description: Version of 19.42 2275 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 1983	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1893	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 466	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 306	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  exdistr  1988  19.42vv  1991  19.42vvv  1993  4exdistr  1995  2sb5  2314  eeeanv  2382  eu6lem  2601  r3ex  3204  rexcom4a  3295  ceqsex2  3503  ceqsex2v  3504  reuind  3713  2reu5lem3  3717  eqvinop  5459  eqvinot  5460  copsexgw  5463  cotsexgw  5466  dfid2  5551  dmopabss  5904  dmopab3  5905  dmxp  5915  rnopabss  5941  rnopab3  5942  dmres  6008  ssrnres  6175  mptpreima  6245  resco  6257  mptfnf  6682  brprcneu  6883  brprcneuALT  6884  fndmin  7052  fliftf  7330  dfoprab2  7485  dmoprab  7530  dmoprabss  7531  fnoprabg  7550  uniuni  7783  zfrep6OLD  7974  opabex3d  7984  opabex3rd  7985  opabex3  7986  fsplit  8138  eroveu  8844  ensymfib  9210  rankuni  9889  aceq1  10206  dfac3  10210  kmlem14  10252  kmlem15  10253  axdc2lem  10536  1idpr  11124  ltexprlem1  11131  ltexprlem4  11134  xpcogend  15139  shftdm  15236  joindm  18559  meetdm  18573  toprntopon  23255  ntreq0  23407  cnextf  24397  dmcuts  28189  adjeu  32503  rexunirn  33142  fpwrelmapffslem  33377  mxidlnzrb  34057  tgoldbachgt  35345  bnj1019  35463  bnj1209  35479  bnj1033  35652  bnj1189  35692  karddom  35900  kardsdom  35901  vonf1oonfo  36003  satfdm  36255  dfiota3  36812  brimg  36826  funpartlem  36833  bj-eeanvw  37744  bj-snsetex  38003  bj-snglc  38009  bj-dfres2  38089  bj-bm1.3ii  38118  bj-dfid2ALT  38119  bj-axreprepsep  38130  bj-restuni  38157  bj-xpcossxp  38250  bj-imdirco  38251  itg2addnc  38732  impprop  38784  dfprop1  38785  sbccom2lem  39196  eldmres  39349  rnxrn  39493  coss1cnvres  39579  nnoeomeqom  44454  rp-isfinite6  44659  undmrnresiss  44744  elintima  44793  pm11.58  45514  pm11.71  45521  2sbc5g  45540  iotasbc2  45543  ax6e2nd  45680  ax6e2ndVD  46029  ax6e2ndALT  46051  modelaxreplem3  46109  stoweidlem60  47209  coxp  50083  mofeu  50098  uobffth  50473  uobeqw  50474  elpglem3  51020