Theorem 19.41v 1946

Description: Version of 19.41 2233 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1966. (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 1883	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1909	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 618	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 474	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1914	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 410	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 211	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777

This theorem is referenced by:  19.41vv  1947  19.41vvv  1948  19.41vvvv  1949  19.42v  1950  exdistrv  1952  equsexvwOLD  2008  r19.41v  3347  gencbvex  3549  euxfrw  3711  euxfr  3713  euind  3714  dfdif3  4090  zfpair  5313  opabn0  5432  eliunxp  5702  relop  5715  dmuni  5777  dminss  6004  imainss  6005  cnvresima  6081  rnco  6099  coass  6112  xpco  6134  rnoprab  7251  f11o  7642  frxp  7814  omeu  8205  domen  8516  xpassen  8605  kmlem3  9572  cflem  9662  genpass  10425  ltexprlem4  10455  hasheqf1oi  13706  elwspths2spth  27740  bnj534  32005  bnj906  32197  bnj908  32198  bnj916  32200  bnj983  32218  bnj986  32222  fmla0  32624  fmlasuc0  32626  dftr6  32981  bj-eeanvw  34042  bj-csbsnlem  34215  bj-rest10  34373  bj-restuni  34382  bj-ccinftydisj  34489  wl-dfclab  34822  eldmqsres2  35538  prter2  36011  dihglb2  38472  prjspeclsp  39255  pm11.6  40717  pm11.71  40722  rfcnnnub  41286  eliunxp2  44376