Theorem 19.42v 1955

Description: Version of 19.42 2244 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 1951	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1863	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 303	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  exdistr  1956  19.42vv  1959  19.42vvv  1961  4exdistr  1963  2sb5  2285  eeeanv  2355  eu6lem  2574  r3ex  3177  rexcom4a  3268  ceqsex2  3495  ceqsex2v  3496  reuind  3713  2reu5lem3  3717  sbccomlemOLD  3822  bm1.3iiOLD  5249  eqvinop  5443  dfid2  5529  dmopabss  5875  dmopab3  5876  dmxp  5886  rnopabss  5912  rnopab3  5913  dmres  5979  ssrnres  6144  mptpreima  6204  resco  6216  mptfnf  6635  brprcneu  6832  brprcneuALT  6833  fndmin  6999  fliftf  7271  dfoprab2  7426  dmoprab  7471  dmoprabss  7472  fnoprabg  7491  uniuni  7717  zfrep6  7909  opabex3d  7919  opabex3rd  7920  opabex3  7921  fsplit  8069  eroveu  8761  ensymfib  9120  rankuni  9787  aceq1  10039  dfac3  10043  kmlem14  10086  kmlem15  10087  axdc2lem  10370  1idpr  10952  ltexprlem1  10959  ltexprlem4  10962  xpcogend  14909  shftdm  15006  joindm  18308  meetdm  18322  toprntopon  22881  ntreq0  23033  cnextf  24022  dmcuts  27799  adjeu  31977  rexunirn  32578  fpwrelmapffslem  32822  mxidlnzrb  33573  tgoldbachgt  34841  bnj1019  34956  bnj1209  34972  bnj1033  35145  bnj1189  35185  satfdm  35585  dfiota3  36137  brimg  36151  funpartlem  36158  bj-eeanvw  36958  bj-snsetex  37211  bj-snglc  37217  bj-bm1.3ii  37312  bj-dfid2ALT  37313  bj-axreprepsep  37323  bj-restuni  37350  bj-xpcossxp  37444  bj-imdirco  37445  itg2addnc  37925  sbccom2lem  38375  eldmres  38528  rnxrn  38672  coss1cnvres  38758  nnoeomeqom  43669  rp-isfinite6  43874  undmrnresiss  43960  elintima  44009  pm11.58  44746  pm11.71  44753  2sbc5g  44772  iotasbc2  44776  ax6e2nd  44914  ax6e2ndVD  45263  ax6e2ndALT  45285  modelaxreplem3  45336  stoweidlem60  46418  coxp  49192  mofeu  49207  uobffth  49577  uobeqw  49578  elpglem3  50072