Theorem 19.42v 1988

Description: Version of 19.42 2276 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 1984	. 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 1945

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

This theorem is used by:  exdistr  1989  19.42vv  1992  19.42vvv  1994  4exdistr  1996  2sb5  2315  eeeanv  2383  eu6lem  2601  r3ex  3205  rexcom4a  3296  ceqsex2  3504  ceqsex2v  3505  reuind  3714  2reu5lem3  3718  eqvinop  5463  eqvinot  5464  copsexgw  5467  cotsexgw  5470  dfid2  5555  dmopabss  5912  dmopab3  5913  dmxp  5923  rnopabss  5949  rnopab3  5950  dmres  6020  ssrnres  6188  mptpreima  6258  resco  6270  mptfnf  6704  brprcneu  6906  brprcneuALT  6907  fndmin  7075  fliftf  7354  dfoprab2  7509  dmoprab  7554  dmoprabss  7555  fnoprabg  7574  uniuni  7808  zfrep6OLD  8001  opabex3d  8011  opabex3rd  8012  opabex3  8013  fsplit  8165  eroveu  8871  ensymfib  9237  rankuni  9916  aceq1  10235  dfac3  10239  kmlem14  10281  kmlem15  10282  axdc2lem  10565  1idpr  11153  ltexprlem1  11160  ltexprlem4  11163  xpcogend  15170  shftdm  15267  joindm  18597  meetdm  18611  toprntopon  23298  ntreq0  23450  cnextf  24440  dmcuts  28234  adjeu  32548  rexunirn  33187  fpwrelmapffslem  33420  mxidlnzrb  34108  tgoldbachgt  35403  bnj1019  35521  bnj1209  35537  bnj1033  35710  bnj1189  35750  karddom  35970  kardsdom  35971  vonf1oonfo  36090  satfdm  36342  dfiota3  36900  brimg  36914  funpartlem  36921  bj-eeanvw  37832  bj-snsetex  38091  bj-snglc  38097  bj-dfres2  38185  bj-bm1.3ii  38249  bj-dfid2ALT  38250  bj-axreprepsep  38261  bj-restuni  38288  bj-xpcossxp  38378  bj-imdirco  38379  itg2addnc  38860  impprop  38912  dfprop1  38913  sbccom2lem  39322  eldmres  39475  rnxrn  39619  coss1cnvres  39705  nnoeomeqom  44575  rp-isfinite6  44780  undmrnresiss  44865  elintima  44914  pm11.58  45635  pm11.71  45642  2sbc5g  45661  iotasbc2  45664  ax6e2nd  45801  ax6e2ndVD  46150  ax6e2ndALT  46172  modelaxreplem3  46234  stoweidlem60  47343  coxp  50275  mofeu  50290  uobffth  50665  uobeqw  50666  elpglem3  51212