Theorem 19.42v 1957

Description: Version of 19.42 2229 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 1953	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1864	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 461	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 302	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  exdistr  1958  19.42vv  1961  19.42vvv  1963  4exdistr  1965  2sb5  2271  eeeanv  2346  eu6lem  2566  rexcom4a  3288  cbvrexdva2OLD  3345  ceqsex2  3526  ceqsex2v  3527  reuind  3745  2reu5lem3  3749  sbccomlem  3860  bm1.3ii  5295  eqvinop  5480  dfid2  5569  dmopabss  5910  dmopab3  5911  dmres  5995  ssrnres  6166  mptpreima  6226  resco  6238  mptfnf  6672  brprcneu  6868  brprcneuALT  6869  fndmin  7031  fliftf  7296  dfoprab2  7451  dmoprab  7494  dmoprabss  7495  fnoprabg  7515  uniuni  7732  zfrep6  7923  opabex3d  7934  opabex3rd  7935  opabex3  7936  fsplit  8085  eroveu  8789  rexdif1enOLD  9142  ensymfib  9170  rankuni  9840  aceq1  10094  dfac3  10098  kmlem14  10140  kmlem15  10141  axdc2lem  10425  1idpr  11006  ltexprlem1  11013  ltexprlem4  11016  xpcogend  14903  shftdm  15000  joindm  18310  meetdm  18324  toprntopon  22356  ntreq0  22510  cnextf  23499  dmscut  27238  adjeu  31005  rexunirn  31595  fpwrelmapffslem  31828  mxidlnzrb  32441  tgoldbachgt  33506  bnj1019  33621  bnj1209  33638  bnj1033  33811  bnj1189  33851  satfdm  34191  dfiota3  34725  brimg  34739  funpartlem  34744  bj-eeanvw  35395  bj-snsetex  35648  bj-snglc  35654  bj-bm1.3ii  35749  bj-dfid2ALT  35750  bj-restuni  35782  bj-xpcossxp  35874  bj-imdirco  35875  itg2addnc  36346  sbccom2lem  36797  eldmres  36943  rnxrn  37073  coss1cnvres  37092  nnoeomeqom  41833  rp-isfinite6  42040  undmrnresiss  42126  elintima  42175  pm11.58  42920  pm11.71  42927  2sbc5g  42946  iotasbc2  42950  ax6e2nd  43090  ax6e2ndVD  43440  ax6e2ndALT  43462  stoweidlem60  44549  mofeu  47162  elpglem3  47406