Theorem 19.41v 1982

Description: Version of 19.41 2274 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  3198  gencbvex  3514  euxfrw  3687  euxfr  3689  euind  3690  dfdif3OLD  4076  zfpair  5397  opabn0  5543  eliunxp  5828  relop  5841  dmuni  5909  dminss  6155  imainss  6156  cnvresima  6236  rnco  6258  rncoOLD  6259  coass  6272  xpco  6297  rnoprab  7528  eloprabga  7532  f11o  7953  frxp  8131  omeu  8579  domen  8967  xpassen  9069  enfii  9180  ttrclselem2  9705  kmlem3  10155  cflem  10247  genpass  11012  ltexprlem4  11042  hasheqf1oi  14407  elwspths2spth  30356  bnj534  35160  bnj906  35350  bnj908  35351  bnj916  35353  bnj983  35371  bnj986  35375  fmla0  35895  fmlasuc0  35897  rexxfr3dALT  36152  dftr6  36264  bj-eeanvw  37381  bj-substw  37391  bj-csbsnlem  37579  bj-clel3gALT  37725  bj-rest10  37771  bj-restuni  37780  bj-imdirco  37875  bj-ccinftydisj  37898  wl-dfclab  38281  eldmqsres2  38984  disjdmqscossss  39596  prter2  39696  dihglb2  42157  prjspeclsp  43385  pm11.6  45143  pm11.71  45148  rfcnnnub  45797  eliunxp2  49155  thinccic  50290