Theorem 19.42v 1960

Description: Version of 19.42 2237 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 1867	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 464	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 306	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃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 1916

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787

This theorem is referenced by:  exdistr  1961  19.42vv  1964  19.42vvv  1966  4exdistr  1968  2sb5  2279  eeeanv  2352  eu6lem  2574  rexcom4a  3164  cbvrexdva2  3358  ceqsex2  3446  ceqsex2v  3447  reuind  3650  2reu5lem3  3654  sbccomlem  3759  bm1.3ii  5167  eqvinop  5341  dmopabss  5755  dmopab3  5756  dmres  5841  ssrnres  6004  mptpreima  6064  resco  6077  mptfnf  6466  brprcneu  6659  fvprc  6660  fndmin  6816  fliftf  7075  dfoprab2  7220  dmoprab  7263  dmoprabss  7264  fnoprabg  7283  uniuni  7497  zfrep6  7674  opabex3d  7684  opabex3rd  7685  opabex3  7686  fsplit  7831  fsplitOLD  7832  eroveu  8416  rexdif1en  8753  ensymfib  8775  rankuni  9358  aceq1  9610  dfac3  9614  kmlem14  9656  kmlem15  9657  axdc2lem  9941  1idpr  10522  ltexprlem1  10529  ltexprlem4  10532  xpcogend  14416  shftdm  14513  joindm  17722  meetdm  17736  toprntopon  21669  ntreq0  21821  cnextf  22810  adjeu  29816  rexunirn  30406  fpwrelmapffslem  30634  mxidlnzrb  31208  tgoldbachgt  32205  bnj1019  32322  bnj1209  32339  bnj1033  32512  bnj1189  32552  satfdm  32894  dmscut  33638  dfiota3  33855  brimg  33869  funpartlem  33874  bj-eeanvw  34522  bj-snsetex  34765  bj-snglc  34771  bj-bm1.3ii  34847  bj-restuni  34878  bj-xpcossxp  34970  bj-imdirco  34971  itg2addnc  35443  sbccom2lem  35894  eldmres  36020  rnxrn  36136  rp-isfinite6  40663  undmrnresiss  40741  elintima  40791  pm11.58  41530  pm11.71  41537  2sbc5g  41556  iotasbc2  41560  ax6e2nd  41700  ax6e2ndVD  42050  ax6e2ndALT  42072  stoweidlem60  43127  elpglem3  45855