Theorem 19.42v 1986

Description: Version of 19.42 2272 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 1982	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1894	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 466	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 306	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  exdistr  1987  19.42vv  1990  19.42vvv  1992  4exdistr  1994  2sb5  2311  eeeanv  2379  eu6lem  2598  r3ex  3201  rexcom4a  3292  ceqsex2  3500  ceqsex2v  3501  reuind  3711  2reu5lem3  3715  bm1.3iiOLD  5259  eqvinop  5463  copsexgw  5466  dfid2  5552  dmopabss  5902  dmopab3  5903  dmxp  5913  rnopabss  5939  rnopab3  5940  dmres  6005  ssrnres  6171  mptpreima  6234  resco  6246  mptfnf  6668  brprcneu  6869  brprcneuALT  6870  fndmin  7038  fliftf  7317  dfoprab2  7472  dmoprab  7517  dmoprabss  7518  fnoprabg  7537  uniuni  7762  zfrep6OLD  7953  opabex3d  7963  opabex3rd  7964  opabex3  7965  fsplit  8115  eroveu  8813  ensymfib  9179  rankuni  9846  aceq1  10121  dfac3  10125  kmlem14  10167  kmlem15  10168  axdc2lem  10451  1idpr  11039  ltexprlem1  11046  ltexprlem4  11049  xpcogend  15048  shftdm  15145  joindm  18462  meetdm  18476  toprntopon  23151  ntreq0  23303  cnextf  24293  dmcuts  28057  adjeu  32371  rexunirn  32968  fpwrelmapffslem  33204  mxidlnzrb  33883  tgoldbachgt  35172  bnj1019  35290  bnj1209  35306  bnj1033  35479  bnj1189  35519  karddom  35688  kardsdom  35689  vonf1oonfo  35713  satfdm  35949  dfiota3  36501  brimg  36515  funpartlem  36522  bj-eeanvw  37449  bj-snsetex  37708  bj-snglc  37714  bj-bm1.3ii  37809  bj-dfid2ALT  37810  bj-axreprepsep  37821  bj-restuni  37848  bj-xpcossxp  37942  bj-imdirco  37943  itg2addnc  38424  sbccom2lem  38873  eldmres  39026  rnxrn  39170  coss1cnvres  39256  nnoeomeqom  44154  rp-isfinite6  44359  undmrnresiss  44445  elintima  44494  pm11.58  45215  pm11.71  45222  2sbc5g  45241  iotasbc2  45245  ax6e2nd  45382  ax6e2ndVD  45731  ax6e2ndALT  45753  modelaxreplem3  45804  stoweidlem60  46889  coxp  49762  mofeu  49777  uobffth  50145  uobeqw  50146  elpglem3  50640