Theorem 19.41v 1982

Description: Version of 19.41 2273 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 2000. (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 1919	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1945	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 629	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 18	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 477	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1950	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 413	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 212	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  19.41vv  1983  19.41vvv  1984  19.41vvvv  1985  19.42v  1986  exdistrv  1988  r19.41v  3194  gencbvex  3509  euxfrw  3682  euxfr  3684  euind  3685  zfpair  5390  opabn0  5536  eliunxp  5821  relop  5834  dmuni  5902  dminss  6148  imainss  6149  cnvresima  6230  rnco  6252  rncoOLD  6253  coass  6266  xpco  6291  rnoprab  7522  eloprabga  7526  f11o  7948  frxp  8128  omeu  8576  domen  8971  xpassen  9073  enfii  9184  ttrclselem2  9709  kmlem3  10159  cflem  10251  genpass  11022  ltexprlem4  11052  hasheqf1oi  14419  elwspths2spth  30446  bnj534  35257  bnj906  35447  bnj908  35448  bnj916  35450  bnj983  35468  bnj986  35472  fmla0  35969  fmlasuc0  35971  rexxfr3dALT  36226  dftr6  36338  bj-eeanvw  37456  bj-substw  37466  bj-csbsnlem  37654  bj-clel3gALT  37800  bj-rest10  37846  bj-restuni  37855  bj-imdirco  37950  bj-ccinftydisj  37973  wl-dfclab  38356  eldmqsres2  39050  disjdmqscossss  39662  prter2  39762  dihglb2  42223  prjspeclsp  43466  pm11.6  45224  pm11.71  45229  rfcnnnub  45878  eliunxp2  49272  thinccic  50405