Theorem 19.41v 1984

Description: Version of 19.41 2275 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 2002. (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 1921	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1947	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 629	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 18	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 477	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1952	. . 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 1945

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

This theorem is used by:  19.41vv  1985  19.41vvv  1986  19.41vvvv  1987  19.42v  1988  exdistrv  1990  r19.41v  3196  gencbvex  3510  euxfrw  3682  euxfr  3684  euind  3685  zfpair  5388  opabn0  5533  eliunxp  5821  relop  5835  dmuni  5904  dminss  6156  imainss  6157  cnvresima  6245  rnco  6267  rncoOLD  6268  coassOLD  6286  xpco  6313  rnoprab  7551  eloprabga  7555  f11o  7986  frxp  8168  omeu  8624  domen  9019  xpassen  9121  enfii  9232  ttrclselem2  9757  kmlem3  10261  cflem  10353  genpass  11124  ltexprlem4  11154  hasheqf1oi  14525  elwspths2spth  30592  bnj534  35453  bnj906  35643  bnj908  35644  bnj916  35646  bnj983  35664  bnj986  35668  fmla0  36327  fmlasuc0  36329  rexxfr3dALT  36584  mirimanofffr  36642  dftr6  36707  bj-eeanvw  37808  bj-substw  37818  bj-csbsnlem  38006  bj-clel3gALT  38167  bj-rest10  38213  bj-restuni  38222  bj-imdirco  38316  bj-ccinftydisj  38339  wl-dfclab  38722  eldmqsres2  39429  disjdmqscossss  40041  prter2  40141  dihglb2  42602  prjspeclsp  43844  pm11.6  45579  pm11.71  45584  rfcnnnub  46269  eliunxp2  49661  thinccic  50821