Theorem 19.41v 1953

Description: Version of 19.41 2228 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1971. (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 1889	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1915	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 617	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 472	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1920	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 408	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 208	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  19.41vv  1954  19.41vvv  1955  19.41vvvv  1956  19.42v  1957  exdistrv  1959  r19.41v  3276  gencbvex  3488  euxfrw  3656  euxfr  3658  euind  3659  dfdif3  4049  zfpair  5344  opabn0  5466  eliunxp  5746  relop  5759  dmuni  5823  dminss  6056  imainss  6057  cnvresima  6133  rnco  6156  coass  6169  xpco  6192  rnoprab  7378  eloprabga  7382  f11o  7789  frxp  7967  omeu  8416  domen  8751  xpassen  8853  dif1en  8945  enfii  8972  ttrclselem2  9484  kmlem3  9908  cflem  10002  genpass  10765  ltexprlem4  10795  hasheqf1oi  14066  elwspths2spth  28332  bnj534  32719  bnj906  32910  bnj908  32911  bnj916  32913  bnj983  32931  bnj986  32935  fmla0  33344  fmlasuc0  33346  dftr6  33718  bj-eeanvw  34895  bj-substw  34904  bj-csbsnlem  35088  bj-clel3gALT  35221  bj-rest10  35259  bj-restuni  35268  bj-imdirco  35361  bj-ccinftydisj  35384  wl-dfclab  35747  eldmqsres2  36422  prter2  36895  dihglb2  39356  prjspeclsp  40451  pm11.6  42010  pm11.71  42015  rfcnnnub  42579  eliunxp2  45669  thinccic  46342