Theorem 19.42v 1954

Description: Version of 19.42 2239 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 1950	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1862	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 303	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780

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 207  df-an 396  df-ex 1781

This theorem is referenced by:  exdistr  1955  19.42vv  1958  19.42vvv  1960  4exdistr  1962  2sb5  2280  eeeanv  2350  eu6lem  2568  r3ex  3171  rexcom4a  3262  ceqsex2  3489  ceqsex2v  3490  reuind  3707  2reu5lem3  3711  sbccomlemOLD  3816  bm1.3iiOLD  5242  eqvinop  5430  dfid2  5516  dmopabss  5863  dmopab3  5864  dmxp  5874  rnopabss  5900  rnopab3  5901  dmres  5966  ssrnres  6131  mptpreima  6191  resco  6203  mptfnf  6622  brprcneu  6818  brprcneuALT  6819  fndmin  6984  fliftf  7255  dfoprab2  7410  dmoprab  7455  dmoprabss  7456  fnoprabg  7475  uniuni  7701  zfrep6  7893  opabex3d  7903  opabex3rd  7904  opabex3  7905  fsplit  8053  eroveu  8742  ensymfib  9099  rankuni  9762  aceq1  10014  dfac3  10018  kmlem14  10061  kmlem15  10062  axdc2lem  10345  1idpr  10926  ltexprlem1  10933  ltexprlem4  10936  xpcogend  14887  shftdm  14984  joindm  18285  meetdm  18299  toprntopon  22846  ntreq0  22998  cnextf  23987  dmscut  27758  adjeu  31876  rexunirn  32478  fpwrelmapffslem  32722  mxidlnzrb  33452  tgoldbachgt  34683  bnj1019  34798  bnj1209  34815  bnj1033  34988  bnj1189  35028  satfdm  35420  dfiota3  35972  brimg  35986  funpartlem  35993  bj-eeanvw  36764  bj-snsetex  37014  bj-snglc  37020  bj-bm1.3ii  37115  bj-dfid2ALT  37116  bj-restuni  37148  bj-xpcossxp  37240  bj-imdirco  37241  itg2addnc  37720  sbccom2lem  38170  eldmres  38315  rnxrn  38451  coss1cnvres  38525  nnoeomeqom  43410  rp-isfinite6  43616  undmrnresiss  43702  elintima  43751  pm11.58  44488  pm11.71  44495  2sbc5g  44514  iotasbc2  44518  ax6e2nd  44656  ax6e2ndVD  45005  ax6e2ndALT  45027  modelaxreplem3  45078  stoweidlem60  46163  coxp  48938  mofeu  48953  uobffth  49324  uobeqw  49325  elpglem3  49819