Theorem 19.42v 1955

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  exdistr  1956  19.42vv  1959  19.42vvv  1961  4exdistr  1963  2sb5  2285  eeeanv  2355  eu6lem  2574  r3ex  3177  rexcom4a  3268  ceqsex2  3482  ceqsex2v  3483  reuind  3700  2reu5lem3  3704  sbccomlemOLD  3809  bm1.3iiOLD  5238  eqvinop  5436  dfid2  5522  dmopabss  5868  dmopab3  5869  dmxp  5879  rnopabss  5905  rnopab3  5906  dmres  5972  ssrnres  6137  mptpreima  6197  resco  6209  mptfnf  6628  brprcneu  6825  brprcneuALT  6826  fndmin  6992  fliftf  7264  dfoprab2  7419  dmoprab  7464  dmoprabss  7465  fnoprabg  7484  uniuni  7710  zfrep6OLD  7902  opabex3d  7912  opabex3rd  7913  opabex3  7914  fsplit  8061  eroveu  8753  ensymfib  9112  rankuni  9781  aceq1  10033  dfac3  10037  kmlem14  10080  kmlem15  10081  axdc2lem  10364  1idpr  10946  ltexprlem1  10953  ltexprlem4  10956  xpcogend  14930  shftdm  15027  joindm  18333  meetdm  18347  toprntopon  22903  ntreq0  23055  cnextf  24044  dmcuts  27800  adjeu  31978  rexunirn  32579  fpwrelmapffslem  32823  mxidlnzrb  33558  tgoldbachgt  34826  bnj1019  34941  bnj1209  34957  bnj1033  35130  bnj1189  35170  satfdm  35570  dfiota3  36122  brimg  36136  funpartlem  36143  bj-eeanvw  37031  bj-snsetex  37289  bj-snglc  37295  bj-bm1.3ii  37390  bj-dfid2ALT  37391  bj-axreprepsep  37401  bj-restuni  37428  bj-xpcossxp  37522  bj-imdirco  37523  itg2addnc  38012  sbccom2lem  38462  eldmres  38615  rnxrn  38759  coss1cnvres  38845  nnoeomeqom  43761  rp-isfinite6  43966  undmrnresiss  44052  elintima  44101  pm11.58  44838  pm11.71  44845  2sbc5g  44864  iotasbc2  44868  ax6e2nd  45006  ax6e2ndVD  45355  ax6e2ndALT  45377  modelaxreplem3  45428  stoweidlem60  46509  coxp  49323  mofeu  49338  uobffth  49708  uobeqw  49709  elpglem3  50203