Theorem 19.41v 1981

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  19.41vv  1982  19.41vvv  1983  19.41vvvv  1984  19.42v  1985  exdistrv  1987  r19.41v  3192  gencbvex  3506  euxfrw  3678  euxfr  3680  euind  3681  zfpair  5382  opabn0  5527  eliunxp  5813  relop  5827  dmuni  5895  dminss  6142  imainss  6143  cnvresima  6231  rnco  6253  rncoOLD  6254  coass  6267  xpco  6292  rnoprab  7526  eloprabga  7530  f11o  7960  frxp  8141  omeu  8597  domen  8992  xpassen  9094  enfii  9205  ttrclselem2  9731  kmlem3  10235  cflem  10327  genpass  11098  ltexprlem4  11128  hasheqf1oi  14499  elwspths2spth  30565  bnj534  35417  bnj906  35607  bnj908  35608  bnj916  35610  bnj983  35628  bnj986  35632  fmla0  36234  fmlasuc0  36236  rexxfr3dALT  36491  dftr6  36609  bj-eeanvw  37710  bj-substw  37720  bj-csbsnlem  37908  coi1in  38054  bj-clel3gALT  38056  bj-rest10  38102  bj-restuni  38111  bj-imdirco  38205  bj-ccinftydisj  38228  wl-dfclab  38611  eldmqsres2  39320  disjdmqscossss  39932  prter2  40032  dihglb2  42493  prjspeclsp  43734  pm11.6  45470  pm11.71  45475  rfcnnnub  46147  eliunxp2  49540  thinccic  50700