Theorem 19.42v 1973

Description: Version of 19.42 2271 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 1969	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1881	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 464	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 305	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800

This theorem is referenced by:  exdistr  1974  19.42vv  1977  19.42vvv  1979  4exdistr  1981  2sb5  2312  eeeanv  2381  eu6lem  2600  r3ex  3201  rexcom4a  3292  ceqsex2  3504  ceqsex2v  3505  reuind  3716  2reu5lem3  3720  sbccomlemOLD  3823  bm1.3iiOLD  5252  eqvinop  5455  copsexgw  5458  dfid2  5544  dmopabss  5894  dmopab3  5895  dmxp  5905  rnopabss  5931  rnopab3  5932  dmres  5998  ssrnres  6164  mptpreima  6225  resco  6237  mptfnf  6656  brprcneu  6857  brprcneuALT  6858  fndmin  7026  fliftf  7299  dfoprab2  7454  dmoprab  7499  dmoprabss  7500  fnoprabg  7519  uniuni  7745  zfrep6OLD  7936  opabex3d  7946  opabex3rd  7947  opabex3  7948  fsplit  8096  eroveu  8794  ensymfib  9152  rankuni  9821  aceq1  10073  dfac3  10077  kmlem14  10120  kmlem15  10121  axdc2lem  10405  1idpr  10987  ltexprlem1  10994  ltexprlem4  10997  xpcogend  14987  shftdm  15084  joindm  18405  meetdm  18419  toprntopon  22985  ntreq0  23137  cnextf  24126  dmcuts  27884  adjeu  32092  rexunirn  32691  fpwrelmapffslem  32934  mxidlnzrb  33668  tgoldbachgt  34957  bnj1019  35075  bnj1209  35091  bnj1033  35264  bnj1189  35304  vonf1oonfo  35458  satfdm  35719  dfiota3  36271  brimg  36285  funpartlem  36292  bj-eeanvw  37190  bj-snsetex  37448  bj-snglc  37454  bj-bm1.3ii  37549  bj-dfid2ALT  37550  bj-axreprepsep  37560  bj-restuni  37587  bj-xpcossxp  37681  bj-imdirco  37682  itg2addnc  38173  sbccom2lem  38623  eldmres  38776  rnxrn  38920  coss1cnvres  39006  nnoeomeqom  43889  rp-isfinite6  44094  undmrnresiss  44180  elintima  44229  pm11.58  44966  pm11.71  44973  2sbc5g  44992  iotasbc2  44996  ax6e2nd  45134  ax6e2ndVD  45483  ax6e2ndALT  45505  modelaxreplem3  45556  stoweidlem60  46634  coxp  49454  mofeu  49469  uobffth  49839  uobeqw  49840  elpglem3  50334