Theorem 19.42v 1986

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 1982	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1894	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 466	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 306	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  exdistr  1987  19.42vv  1990  19.42vvv  1992  4exdistr  1994  2sb5  2315  eeeanv  2384  eu6lem  2603  r3ex  3206  rexcom4a  3297  ceqsex2  3507  ceqsex2v  3508  reuind  3718  2reu5lem3  3722  bm1.3iiOLD  5267  eqvinop  5471  copsexgw  5474  dfid2  5560  dmopabss  5910  dmopab3  5911  dmxp  5921  rnopabss  5947  rnopab3  5948  dmres  6013  ssrnres  6178  mptpreima  6241  resco  6253  mptfnf  6674  brprcneu  6875  brprcneuALT  6876  fndmin  7044  fliftf  7322  dfoprab2  7477  dmoprab  7522  dmoprabss  7523  fnoprabg  7542  uniuni  7767  zfrep6OLD  7958  opabex3d  7968  opabex3rd  7969  opabex3  7970  fsplit  8118  eroveu  8816  ensymfib  9175  rankuni  9842  aceq1  10117  dfac3  10121  kmlem14  10163  kmlem15  10164  axdc2lem  10447  1idpr  11031  ltexprlem1  11038  ltexprlem4  11041  xpcogend  15037  shftdm  15134  joindm  18453  meetdm  18467  toprntopon  23134  ntreq0  23286  cnextf  24276  dmcuts  28037  adjeu  32314  rexunirn  32911  fpwrelmapffslem  33149  mxidlnzrb  33828  tgoldbachgt  35117  bnj1019  35235  bnj1209  35251  bnj1033  35424  bnj1189  35464  karddom  35633  kardsdom  35634  vonf1oonfo  35658  satfdm  35900  dfiota3  36452  brimg  36466  funpartlem  36473  bj-eeanvw  37399  bj-snsetex  37658  bj-snglc  37664  bj-bm1.3ii  37759  bj-dfid2ALT  37760  bj-axreprepsep  37771  bj-restuni  37798  bj-xpcossxp  37892  bj-imdirco  37893  itg2addnc  38384  sbccom2lem  38833  eldmres  38986  rnxrn  39130  coss1cnvres  39216  nnoeomeqom  44099  rp-isfinite6  44304  undmrnresiss  44390  elintima  44439  pm11.58  45160  pm11.71  45167  2sbc5g  45186  iotasbc2  45190  ax6e2nd  45327  ax6e2ndVD  45676  ax6e2ndALT  45698  modelaxreplem3  45749  stoweidlem60  46834  coxp  49670  mofeu  49685  uobffth  50055  uobeqw  50056  elpglem3  50550