Theorem 19.42v 1960

Description: Version of 19.42 2248 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 1956	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1868	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 461	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 304	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  exdistr  1961  19.42vv  1964  19.42vvv  1966  4exdistr  1968  2sb5  2289  eeeanv  2358  eu6lem  2577  r3ex  3178  rexcom4a  3269  ceqsex2  3482  ceqsex2v  3483  reuind  3694  2reu5lem3  3698  sbccomlemOLD  3802  bm1.3iiOLD  5224  eqvinop  5427  copsexgw  5430  dfid2  5515  dmopabss  5860  dmopab3  5861  dmxp  5871  rnopabss  5897  rnopab3  5898  dmres  5964  ssrnres  6129  mptpreima  6189  resco  6201  mptfnf  6620  brprcneu  6817  brprcneuALT  6818  fndmin  6986  fliftf  7259  dfoprab2  7414  dmoprab  7459  dmoprabss  7460  fnoprabg  7479  uniuni  7705  zfrep6OLD  7897  opabex3d  7907  opabex3rd  7908  opabex3  7909  fsplit  8056  eroveu  8749  ensymfib  9108  rankuni  9778  aceq1  10030  dfac3  10034  kmlem14  10077  kmlem15  10078  axdc2lem  10361  1idpr  10943  ltexprlem1  10950  ltexprlem4  10953  xpcogend  14927  shftdm  15024  joindm  18330  meetdm  18344  toprntopon  22908  ntreq0  23060  cnextf  24049  dmcuts  27801  adjeu  31978  rexunirn  32579  fpwrelmapffslem  32824  mxidlnzrb  33563  tgoldbachgt  34847  bnj1019  34962  bnj1209  34978  bnj1033  35151  bnj1189  35191  satfdm  35597  dfiota3  36149  brimg  36163  funpartlem  36170  bj-eeanvw  37058  bj-snsetex  37316  bj-snglc  37322  bj-bm1.3ii  37417  bj-dfid2ALT  37418  bj-axreprepsep  37428  bj-restuni  37455  bj-xpcossxp  37549  bj-imdirco  37550  itg2addnc  38041  sbccom2lem  38491  eldmres  38644  rnxrn  38788  coss1cnvres  38874  nnoeomeqom  43757  rp-isfinite6  43962  undmrnresiss  44048  elintima  44097  pm11.58  44834  pm11.71  44841  2sbc5g  44860  iotasbc2  44864  ax6e2nd  45002  ax6e2ndVD  45351  ax6e2ndALT  45373  modelaxreplem3  45424  stoweidlem60  46503  coxp  49323  mofeu  49338  uobffth  49708  uobeqw  49709  elpglem3  50203