Theorem 19.42v 1986

Description: Version of 19.42 2273 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  2312  eeeanv  2380  eu6lem  2599  r3ex  3202  rexcom4a  3293  ceqsex2  3501  ceqsex2v  3502  reuind  3711  2reu5lem3  3715  eqvinop  5456  eqvinot  5457  copsexgw  5460  cotsexgw  5463  dfid2  5548  dmopabss  5900  dmopab3  5901  dmxp  5911  rnopabss  5937  rnopab3  5938  dmres  6003  ssrnres  6170  mptpreima  6239  resco  6251  mptfnf  6674  brprcneu  6875  brprcneuALT  6876  fndmin  7044  fliftf  7323  dfoprab2  7478  dmoprab  7523  dmoprabss  7524  fnoprabg  7543  uniuni  7776  zfrep6OLD  7967  opabex3d  7977  opabex3rd  7978  opabex3  7979  fsplit  8128  eroveu  8833  ensymfib  9199  rankuni  9879  aceq1  10196  dfac3  10200  kmlem14  10242  kmlem15  10243  axdc2lem  10526  1idpr  11114  ltexprlem1  11121  ltexprlem4  11124  xpcogend  15127  shftdm  15224  joindm  18547  meetdm  18561  toprntopon  23243  ntreq0  23395  cnextf  24385  dmcuts  28177  adjeu  32491  rexunirn  33088  fpwrelmapffslem  33324  mxidlnzrb  34004  tgoldbachgt  35292  bnj1019  35410  bnj1209  35426  bnj1033  35599  bnj1189  35639  karddom  35829  kardsdom  35830  vonf1oonfo  35898  satfdm  36134  dfiota3  36685  brimg  36699  funpartlem  36706  bj-eeanvw  37617  bj-snsetex  37876  bj-snglc  37882  bj-bm1.3ii  37979  bj-dfid2ALT  37980  bj-axreprepsep  37991  bj-restuni  38018  bj-xpcossxp  38110  bj-imdirco  38111  itg2addnc  38592  impprop  38644  dfprop1  38645  sbccom2lem  39056  eldmres  39209  rnxrn  39353  coss1cnvres  39439  nnoeomeqom  44313  rp-isfinite6  44518  undmrnresiss  44603  elintima  44652  pm11.58  45373  pm11.71  45380  2sbc5g  45399  iotasbc2  45403  ax6e2nd  45540  ax6e2ndVD  45889  ax6e2ndALT  45911  modelaxreplem3  45969  stoweidlem60  47069  coxp  49942  mofeu  49957  uobffth  50325  uobeqw  50326  elpglem3  50805