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 618	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 473	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1920	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 409	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 208	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 397  ∃wex 1781

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782

This theorem is referenced by:  19.41vv  1954  19.41vvv  1955  19.41vvvv  1956  19.42v  1957  exdistrv  1959  r19.41v  3182  gencbvex  3500  euxfrw  3670  euxfr  3672  euind  3673  dfdif3  4065  zfpair  5368  opabn0  5501  eliunxp  5783  relop  5796  dmuni  5860  dminss  6095  imainss  6096  cnvresima  6172  rnco  6194  coass  6207  xpco  6231  rnoprab  7444  eloprabga  7448  f11o  7861  frxp  8038  omeu  8491  domen  8826  xpassen  8935  dif1enOLD  9031  enfii  9058  ttrclselem2  9587  kmlem3  10013  cflem  10107  genpass  10870  ltexprlem4  10900  hasheqf1oi  14170  elwspths2spth  28619  bnj534  33016  bnj906  33207  bnj908  33208  bnj916  33210  bnj983  33228  bnj986  33232  fmla0  33641  fmlasuc0  33643  dftr6  34007  bj-eeanvw  35032  bj-substw  35041  bj-csbsnlem  35224  bj-clel3gALT  35373  bj-rest10  35413  bj-restuni  35422  bj-imdirco  35515  bj-ccinftydisj  35538  wl-dfclab  35903  eldmqsres2  36604  disjdmqscossss  37121  prter2  37199  dihglb2  39661  prjspeclsp  40762  pm11.6  42383  pm11.71  42388  rfcnnnub  42952  eliunxp2  46087  thinccic  46760