Theorem 19.42v 1957

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃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 1913

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

This theorem is referenced by:  exdistr  1958  19.42vv  1961  19.42vvv  1963  4exdistr  1965  2sb5  2272  eeeanv  2348  eu6lem  2573  rexcom4a  3236  cbvrexdva2  3393  ceqsex2  3482  ceqsex2v  3483  reuind  3688  2reu5lem3  3692  sbccomlem  3803  bm1.3ii  5226  eqvinop  5401  dfid2  5491  dmopabss  5827  dmopab3  5828  dmres  5913  ssrnres  6081  mptpreima  6141  resco  6154  mptfnf  6568  brprcneu  6764  brprcneuALT  6765  fndmin  6922  fliftf  7186  dfoprab2  7333  dmoprab  7376  dmoprabss  7377  fnoprabg  7397  uniuni  7612  zfrep6  7797  opabex3d  7808  opabex3rd  7809  opabex3  7810  fsplit  7957  fsplitOLD  7958  eroveu  8601  rexdif1en  8944  ensymfib  8970  rankuni  9621  aceq1  9873  dfac3  9877  kmlem14  9919  kmlem15  9920  axdc2lem  10204  1idpr  10785  ltexprlem1  10792  ltexprlem4  10795  xpcogend  14685  shftdm  14782  joindm  18093  meetdm  18107  toprntopon  22074  ntreq0  22228  cnextf  23217  adjeu  30251  rexunirn  30840  fpwrelmapffslem  31067  mxidlnzrb  31644  tgoldbachgt  32643  bnj1019  32759  bnj1209  32776  bnj1033  32949  bnj1189  32989  satfdm  33331  dmscut  34005  dfiota3  34225  brimg  34239  funpartlem  34244  bj-eeanvw  34895  bj-snsetex  35153  bj-snglc  35159  bj-bm1.3ii  35235  bj-dfid2ALT  35236  bj-restuni  35268  bj-xpcossxp  35360  bj-imdirco  35361  itg2addnc  35831  sbccom2lem  36282  eldmres  36408  rnxrn  36524  rp-isfinite6  41125  undmrnresiss  41212  elintima  41261  pm11.58  42008  pm11.71  42015  2sbc5g  42034  iotasbc2  42038  ax6e2nd  42178  ax6e2ndVD  42528  ax6e2ndALT  42550  stoweidlem60  43601  mofeu  46175  elpglem3  46418