Theorem 19.42v 1954

Description: Version of 19.42 2241 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  2282  eeeanv  2352  eu6lem  2571  r3ex  3173  rexcom4a  3264  ceqsex2  3491  ceqsex2v  3492  reuind  3709  2reu5lem3  3713  sbccomlemOLD  3818  bm1.3iiOLD  5245  eqvinop  5433  dfid2  5519  dmopabss  5865  dmopab3  5866  dmxp  5876  rnopabss  5902  rnopab3  5903  dmres  5969  ssrnres  6134  mptpreima  6194  resco  6206  mptfnf  6625  brprcneu  6822  brprcneuALT  6823  fndmin  6988  fliftf  7259  dfoprab2  7414  dmoprab  7459  dmoprabss  7460  fnoprabg  7479  uniuni  7705  zfrep6  7897  opabex3d  7907  opabex3rd  7908  opabex3  7909  fsplit  8057  eroveu  8747  ensymfib  9106  rankuni  9773  aceq1  10025  dfac3  10029  kmlem14  10072  kmlem15  10073  axdc2lem  10356  1idpr  10938  ltexprlem1  10945  ltexprlem4  10948  xpcogend  14895  shftdm  14992  joindm  18294  meetdm  18308  toprntopon  22867  ntreq0  23019  cnextf  24008  dmscut  27779  adjeu  31913  rexunirn  32515  fpwrelmapffslem  32760  mxidlnzrb  33510  tgoldbachgt  34769  bnj1019  34884  bnj1209  34901  bnj1033  35074  bnj1189  35114  satfdm  35512  dfiota3  36064  brimg  36078  funpartlem  36085  bj-eeanvw  36857  bj-snsetex  37107  bj-snglc  37113  bj-bm1.3ii  37208  bj-dfid2ALT  37209  bj-restuni  37241  bj-xpcossxp  37333  bj-imdirco  37334  itg2addnc  37814  sbccom2lem  38264  eldmres  38409  rnxrn  38545  coss1cnvres  38619  nnoeomeqom  43496  rp-isfinite6  43701  undmrnresiss  43787  elintima  43836  pm11.58  44573  pm11.71  44580  2sbc5g  44599  iotasbc2  44603  ax6e2nd  44741  ax6e2ndVD  45090  ax6e2ndALT  45112  modelaxreplem3  45163  stoweidlem60  46246  coxp  49020  mofeu  49035  uobffth  49405  uobeqw  49406  elpglem3  49900