Theorem 19.41v 1982

Description: Version of 19.41 2272 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  3193  gencbvex  3507  euxfrw  3679  euxfr  3681  euind  3682  zfpair  5383  opabn0  5528  eliunxp  5814  relop  5828  dmuni  5896  dminss  6142  imainss  6143  cnvresima  6224  rnco  6246  rncoOLD  6247  coass  6260  xpco  6285  rnoprab  7517  eloprabga  7521  f11o  7948  frxp  8127  omeu  8577  domen  8972  xpassen  9074  enfii  9185  ttrclselem2  9711  kmlem3  10212  cflem  10304  genpass  11075  ltexprlem4  11105  hasheqf1oi  14475  elwspths2spth  30541  bnj534  35353  bnj906  35543  bnj908  35544  bnj916  35546  bnj983  35564  bnj986  35568  fmla0  36116  fmlasuc0  36118  rexxfr3dALT  36373  dftr6  36485  bj-eeanvw  37587  bj-substw  37597  bj-csbsnlem  37785  bj-clel3gALT  37931  bj-rest10  37977  bj-restuni  37986  bj-imdirco  38079  bj-ccinftydisj  38102  wl-dfclab  38485  eldmqsres2  39194  disjdmqscossss  39806  prter2  39906  dihglb2  42367  prjspeclsp  43602  pm11.6  45335  pm11.71  45340  rfcnnnub  45996  eliunxp2  49390  thinccic  50523