Theorem 19.42v 1953

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  exdistr  1954  19.42vv  1957  19.42vvv  1959  4exdistr  1961  2sb5  2278  eeeanv  2348  eu6lem  2566  r3ex  3168  rexcom4a  3259  ceqsex2  3490  ceqsex2v  3491  reuind  3713  2reu5lem3  3717  sbccomlemOLD  3822  bm1.3iiOLD  5241  eqvinop  5430  dfid2  5516  dmopabss  5861  dmopab3  5862  dmxp  5871  rnopabss  5897  rnopab3  5898  dmres  5963  ssrnres  6127  mptpreima  6187  resco  6199  mptfnf  6617  brprcneu  6812  brprcneuALT  6813  fndmin  6979  fliftf  7252  dfoprab2  7407  dmoprab  7452  dmoprabss  7453  fnoprabg  7472  uniuni  7698  zfrep6  7890  opabex3d  7900  opabex3rd  7901  opabex3  7902  fsplit  8050  eroveu  8739  ensymfib  9098  rankuni  9759  aceq1  10011  dfac3  10015  kmlem14  10058  kmlem15  10059  axdc2lem  10342  1idpr  10923  ltexprlem1  10930  ltexprlem4  10933  xpcogend  14881  shftdm  14978  joindm  18279  meetdm  18293  toprntopon  22810  ntreq0  22962  cnextf  23951  dmscut  27722  adjeu  31833  rexunirn  32436  fpwrelmapffslem  32675  mxidlnzrb  33417  tgoldbachgt  34631  bnj1019  34746  bnj1209  34763  bnj1033  34936  bnj1189  34976  satfdm  35346  dfiota3  35901  brimg  35915  funpartlem  35920  bj-eeanvw  36691  bj-snsetex  36941  bj-snglc  36947  bj-bm1.3ii  37042  bj-dfid2ALT  37043  bj-restuni  37075  bj-xpcossxp  37167  bj-imdirco  37168  itg2addnc  37658  sbccom2lem  38108  eldmres  38249  rnxrn  38374  coss1cnvres  38398  nnoeomeqom  43289  rp-isfinite6  43495  undmrnresiss  43581  elintima  43630  pm11.58  44367  pm11.71  44374  2sbc5g  44393  iotasbc2  44397  ax6e2nd  44536  ax6e2ndVD  44885  ax6e2ndALT  44907  modelaxreplem3  44958  stoweidlem60  46045  coxp  48821  mofeu  48836  uobffth  49207  uobeqw  49208  elpglem3  49702