Theorem 19.42v 1980

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

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807

This theorem is referenced by:  exdistr  1981  19.42vv  1984  19.42vvv  1986  4exdistr  1988  2sb5  2319  eeeanv  2388  eu6lem  2607  r3ex  3210  rexcom4a  3301  ceqsex2  3513  ceqsex2v  3514  reuind  3725  2reu5lem3  3729  sbccomlemOLD  3832  bm1.3iiOLD  5267  eqvinop  5470  copsexgw  5473  dfid2  5559  dmopabss  5909  dmopab3  5910  dmxp  5920  rnopabss  5946  rnopab3  5947  dmres  6012  ssrnres  6177  mptpreima  6240  resco  6252  mptfnf  6671  brprcneu  6872  brprcneuALT  6873  fndmin  7041  fliftf  7314  dfoprab2  7469  dmoprab  7514  dmoprabss  7515  fnoprabg  7534  uniuni  7761  zfrep6OLD  7952  opabex3d  7962  opabex3rd  7963  opabex3  7964  fsplit  8112  eroveu  8810  ensymfib  9168  rankuni  9835  aceq1  10101  dfac3  10105  kmlem14  10147  kmlem15  10148  axdc2lem  10432  1idpr  11014  ltexprlem1  11021  ltexprlem4  11024  xpcogend  15011  shftdm  15108  joindm  18429  meetdm  18443  toprntopon  23051  ntreq0  23203  cnextf  24192  dmcuts  27950  adjeu  32182  rexunirn  32779  fpwrelmapffslem  33018  mxidlnzrb  33707  tgoldbachgt  34995  bnj1019  35113  bnj1209  35129  bnj1033  35302  bnj1189  35342  vonf1oonfo  35498  satfdm  35760  dfiota3  36312  brimg  36326  funpartlem  36333  bj-eeanvw  37229  bj-snsetex  37487  bj-snglc  37493  bj-bm1.3ii  37588  bj-dfid2ALT  37589  bj-axreprepsep  37600  bj-restuni  37627  bj-xpcossxp  37721  bj-imdirco  37722  itg2addnc  38213  sbccom2lem  38663  eldmres  38816  rnxrn  38960  coss1cnvres  39046  nnoeomeqom  43931  rp-isfinite6  44136  undmrnresiss  44222  elintima  44271  pm11.58  44992  pm11.71  44999  2sbc5g  45018  iotasbc2  45022  ax6e2nd  45159  ax6e2ndVD  45508  ax6e2ndALT  45530  modelaxreplem3  45581  stoweidlem60  46666  coxp  49496  mofeu  49511  uobffth  49881  uobeqw  49882  elpglem3  50376