Theorem 19.42v 2048

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

Syntax hints:   ↔ wb 197   ∧ wa 384  ∃wex 1874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875

This theorem is referenced by:  exdistr  2049  19.42vv  2051  19.42vvv  2052  4exdistr  2055  2sb5  2289  eeeanv  2347  eu6  2589  rexcom4a  3379  ceqsex2  3397  reuind  3572  2reu5lem3  3576  sbccomlem  3667  bm1.3ii  4944  eqvinop  5110  dmopabss  5504  dmopab3  5505  dmres  5594  elridOLD  5635  ssrnres  5755  mptpreima  5814  resco  5825  mptfnf  6193  brprcneu  6367  fndmin  6514  fliftf  6757  dfoprab2  6899  dmoprab  6939  dmoprabss  6940  fnoprabg  6959  uniuni  7169  zfrep6  7332  opabex3d  7343  opabex3  7344  fsplit  7484  eroveu  8046  rankuni  8941  aceq1  9191  dfac3  9195  kmlem14  9238  kmlem15  9239  axdc2lem  9523  1idpr  10104  ltexprlem1  10111  ltexprlem4  10114  xpcogend  14000  shftdm  14096  joindm  17269  meetdm  17283  toprntopon  21009  ntreq0  21161  cnextf  22149  adjeu  29204  rexunirn  29785  fpwrelmapffslem  29956  tgoldbachgt  31192  bnj1019  31298  bnj1209  31315  bnj1033  31485  bnj1189  31525  dmscut  32362  dfiota3  32474  brimg  32488  funpartlem  32493  bj-eeanvw  33139  bj-rexcom4  33294  bj-rexcom4a  33295  bj-snsetex  33378  bj-snglc  33384  bj-bm1.3ii  33451  bj-restuni  33478  itg2addnc  33887  sbccom2lem  34350  eldmres  34468  rnxrn  34585  rp-isfinite6  38539  undmrnresiss  38585  elintima  38620  pm11.58  39264  pm11.71  39271  2sbc5g  39290  iotasbc2  39294  ax6e2nd  39436  ax6e2ndVD  39796  ax6e2ndALT  39818  stoweidlem60  40914  elpglem3  43128