Theorem 19.42v 1983

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 1979	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1891	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 465	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 306	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  exdistr  1984  19.42vv  1987  19.42vvv  1989  4exdistr  1991  2sb5  2313  eeeanv  2382  eu6lem  2601  r3ex  3204  rexcom4a  3295  ceqsex2  3505  ceqsex2v  3506  reuind  3716  2reu5lem3  3720  sbccomlemOLD  3823  bm1.3iiOLD  5265  eqvinop  5469  copsexgw  5472  dfid2  5558  dmopabss  5908  dmopab3  5909  dmxp  5919  rnopabss  5945  rnopab3  5946  dmres  6011  ssrnres  6176  mptpreima  6239  resco  6251  mptfnf  6670  brprcneu  6871  brprcneuALT  6872  fndmin  7040  fliftf  7313  dfoprab2  7468  dmoprab  7513  dmoprabss  7514  fnoprabg  7533  uniuni  7757  zfrep6OLD  7948  opabex3d  7958  opabex3rd  7959  opabex3  7960  fsplit  8108  eroveu  8806  ensymfib  9164  rankuni  9831  aceq1  10097  dfac3  10101  kmlem14  10143  kmlem15  10144  axdc2lem  10427  1idpr  11009  ltexprlem1  11016  ltexprlem4  11019  xpcogend  15007  shftdm  15104  joindm  18424  meetdm  18438  toprntopon  23082  ntreq0  23234  cnextf  24223  dmcuts  27984  adjeu  32241  rexunirn  32838  fpwrelmapffslem  33077  mxidlnzrb  33762  tgoldbachgt  35050  bnj1019  35168  bnj1209  35184  bnj1033  35357  bnj1189  35397  karddom  35574  kardsdom  35575  vonf1oonfo  35599  satfdm  35861  dfiota3  36413  brimg  36427  funpartlem  36434  bj-eeanvw  37360  bj-snsetex  37619  bj-snglc  37625  bj-bm1.3ii  37720  bj-dfid2ALT  37721  bj-axreprepsep  37732  bj-restuni  37759  bj-xpcossxp  37853  bj-imdirco  37854  itg2addnc  38345  sbccom2lem  38793  eldmres  38946  rnxrn  39090  coss1cnvres  39176  nnoeomeqom  44059  rp-isfinite6  44264  undmrnresiss  44350  elintima  44399  pm11.58  45120  pm11.71  45127  2sbc5g  45146  iotasbc2  45150  ax6e2nd  45287  ax6e2ndVD  45636  ax6e2ndALT  45658  modelaxreplem3  45709  stoweidlem60  46794  coxp  49631  mofeu  49646  uobffth  50016  uobeqw  50017  elpglem3  50511