Theorem 19.41v 1968

Description: Version of 19.41 2269 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1986. (Revised by Rohan Ridenour, 15-Apr-2022.)

Assertion

Ref	Expression
19.41v	⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.41v

Step	Hyp	Ref	Expression
1		19.40 1905	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1931	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 626	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 475	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1936	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 411	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 211	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  19.41vv  1969  19.41vvv  1970  19.41vvvv  1971  19.42v  1972  exdistrv  1974  r19.41v  3191  gencbvex  3509  euxfrw  3682  euxfr  3684  euind  3685  dfdif3OLD  4070  zfpair  5375  opabn0  5520  eliunxp  5805  relop  5818  dmuni  5886  dminss  6133  imainss  6134  cnvresima  6211  rnco  6233  rncoOLD  6234  coass  6247  xpco  6270  rnoprab  7495  eloprabga  7499  f11o  7922  frxp  8099  omeu  8547  domen  8935  xpassen  9036  enfii  9147  ttrclselem2  9674  kmlem3  10102  cflem  10194  cflemOLD  10195  genpass  10960  ltexprlem4  10990  hasheqf1oi  14357  elwspths2spth  30126  bnj534  34995  bnj906  35185  bnj908  35186  bnj916  35188  bnj983  35206  bnj986  35210  fmla0  35692  fmlasuc0  35694  rexxfr3dALT  35949  dftr6  36061  bj-eeanvw  37150  bj-substw  37160  bj-csbsnlem  37348  bj-clel3gALT  37493  bj-rest10  37538  bj-restuni  37547  bj-imdirco  37642  bj-ccinftydisj  37665  wl-dfclab  38048  eldmqsres2  38753  disjdmqscossss  39365  prter2  39465  dihglb2  41926  prjspeclsp  43154  pm11.6  44928  pm11.71  44933  rfcnnnub  45576  eliunxp2  48916  thinccic  50052