Theorem 19.42v 1958

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

Syntax hints:   ↔ wb 205   ∧ wa 397  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  exdistr  1959  19.42vv  1962  19.42vvv  1964  4exdistr  1966  2sb5  2272  eeeanv  2347  eu6lem  2568  rexcom4a  3290  cbvrexdva2OLD  3347  ceqsex2  3530  ceqsex2v  3531  reuind  3749  2reu5lem3  3753  sbccomlem  3864  bm1.3ii  5302  eqvinop  5487  dfid2  5576  dmopabss  5917  dmopab3  5918  dmres  6002  ssrnres  6175  mptpreima  6235  resco  6247  mptfnf  6683  brprcneu  6879  brprcneuALT  6880  fndmin  7044  fliftf  7309  dfoprab2  7464  dmoprab  7507  dmoprabss  7508  fnoprabg  7528  uniuni  7746  zfrep6  7938  opabex3d  7949  opabex3rd  7950  opabex3  7951  fsplit  8100  eroveu  8803  rexdif1enOLD  9156  ensymfib  9184  rankuni  9855  aceq1  10109  dfac3  10113  kmlem14  10155  kmlem15  10156  axdc2lem  10440  1idpr  11021  ltexprlem1  11028  ltexprlem4  11031  xpcogend  14918  shftdm  15015  joindm  18325  meetdm  18339  toprntopon  22419  ntreq0  22573  cnextf  23562  dmscut  27302  adjeu  31130  rexunirn  31720  fpwrelmapffslem  31945  mxidlnzrb  32584  tgoldbachgt  33664  bnj1019  33779  bnj1209  33796  bnj1033  33969  bnj1189  34009  satfdm  34349  dfiota3  34884  brimg  34898  funpartlem  34903  bj-eeanvw  35580  bj-snsetex  35833  bj-snglc  35839  bj-bm1.3ii  35934  bj-dfid2ALT  35935  bj-restuni  35967  bj-xpcossxp  36059  bj-imdirco  36060  itg2addnc  36531  sbccom2lem  36981  eldmres  37127  rnxrn  37257  coss1cnvres  37276  nnoeomeqom  42048  rp-isfinite6  42255  undmrnresiss  42341  elintima  42390  pm11.58  43135  pm11.71  43142  2sbc5g  43161  iotasbc2  43165  ax6e2nd  43305  ax6e2ndVD  43655  ax6e2ndALT  43677  stoweidlem60  44763  mofeu  47468  elpglem3  47712