Theorem 19.41v 1949

Description: Version of 19.41 2235 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1967. (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 1886	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1912	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 617	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 471	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1917	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 407	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 209	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  19.42v  1953  exdistrv  1955  r19.41v  3174  gencbvex  3520  euxfrw  3704  euxfr  3706  euind  3707  dfdif3OLD  4093  zfpair  5391  opabn0  5528  eliunxp  5817  relop  5830  dmuni  5894  dminss  6142  imainss  6143  cnvresima  6219  rnco  6241  coass  6254  xpco  6278  rnoprab  7512  eloprabga  7516  f11o  7945  frxp  8125  omeu  8597  domen  8976  xpassen  9080  dif1enOLD  9176  enfii  9200  ttrclselem2  9740  kmlem3  10167  cflem  10259  cflemOLD  10260  genpass  11023  ltexprlem4  11053  hasheqf1oi  14369  elwspths2spth  29949  bnj534  34770  bnj906  34961  bnj908  34962  bnj916  34964  bnj983  34982  bnj986  34986  fmla0  35404  fmlasuc0  35406  rexxfr3dALT  35661  dftr6  35768  bj-eeanvw  36731  bj-substw  36740  bj-csbsnlem  36921  bj-clel3gALT  37066  bj-rest10  37106  bj-restuni  37115  bj-imdirco  37208  bj-ccinftydisj  37231  wl-dfclab  37614  eldmqsres2  38306  disjdmqscossss  38821  prter2  38899  dihglb2  41361  prjspeclsp  42635  pm11.6  44416  pm11.71  44421  rfcnnnub  45060  eliunxp2  48309  thinccic  49357