Theorem 19.42v 1952

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  exdistr  1953  19.42vv  1956  19.42vvv  1958  4exdistr  1960  2sb5  2277  eeeanv  2351  eu6lem  2572  r3ex  3197  rexcom4a  3291  cbvrexdva2OLD  3349  ceqsex2  3534  ceqsex2v  3535  reuind  3758  2reu5lem3  3762  sbccomlemOLD  3869  bm1.3iiOLD  5301  eqvinop  5491  dfid2  5579  dmopabss  5928  dmopab3  5929  dmxp  5938  rnopabss  5965  rnopab3  5966  dmres  6029  ssrnres  6197  mptpreima  6257  resco  6269  mptfnf  6702  brprcneu  6895  brprcneuALT  6896  fndmin  7064  fliftf  7336  dfoprab2  7492  dmoprab  7537  dmoprabss  7538  fnoprabg  7557  uniuni  7783  zfrep6  7980  opabex3d  7991  opabex3rd  7992  opabex3  7993  fsplit  8143  eroveu  8853  rexdif1enOLD  9200  ensymfib  9225  rankuni  9904  aceq1  10158  dfac3  10162  kmlem14  10205  kmlem15  10206  axdc2lem  10489  1idpr  11070  ltexprlem1  11077  ltexprlem4  11080  xpcogend  15014  shftdm  15111  joindm  18421  meetdm  18435  toprntopon  22932  ntreq0  23086  cnextf  24075  dmscut  27857  adjeu  31909  rexunirn  32512  fpwrelmapffslem  32744  mxidlnzrb  33509  tgoldbachgt  34679  bnj1019  34794  bnj1209  34811  bnj1033  34984  bnj1189  35024  satfdm  35375  dfiota3  35925  brimg  35939  funpartlem  35944  bj-eeanvw  36715  bj-snsetex  36965  bj-snglc  36971  bj-bm1.3ii  37066  bj-dfid2ALT  37067  bj-restuni  37099  bj-xpcossxp  37191  bj-imdirco  37192  itg2addnc  37682  sbccom2lem  38132  eldmres  38272  rnxrn  38400  coss1cnvres  38419  nnoeomeqom  43330  rp-isfinite6  43536  undmrnresiss  43622  elintima  43671  pm11.58  44414  pm11.71  44421  2sbc5g  44440  iotasbc2  44444  ax6e2nd  44583  ax6e2ndVD  44933  ax6e2ndALT  44955  modelaxreplem3  45002  stoweidlem60  46080  coxp  48749  mofeu  48762  elpglem3  49287