Theorem 19.41v 1951

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃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 1912

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

This theorem is referenced by:  19.41vv  1952  19.41vvv  1953  19.41vvvv  1954  19.42v  1955  exdistrv  1957  r19.41v  3167  gencbvex  3487  euxfrw  3667  euxfr  3669  euind  3670  dfdif3OLD  4058  zfpair  5363  opabn0  5508  eliunxp  5792  relop  5805  dmuni  5869  dminss  6117  imainss  6118  cnvresima  6194  rnco  6216  rncoOLD  6217  coass  6230  xpco  6253  rnoprab  7472  eloprabga  7476  f11o  7900  frxp  8076  omeu  8520  domen  8908  xpassen  9009  enfii  9120  ttrclselem2  9647  kmlem3  10075  cflem  10167  cflemOLD  10168  genpass  10932  ltexprlem4  10962  hasheqf1oi  14313  elwspths2spth  30038  bnj534  34882  bnj906  35072  bnj908  35073  bnj916  35075  bnj983  35093  bnj986  35097  fmla0  35564  fmlasuc0  35566  rexxfr3dALT  35821  dftr6  35933  bj-eeanvw  37012  bj-substw  37022  bj-csbsnlem  37210  bj-clel3gALT  37355  bj-rest10  37400  bj-restuni  37409  bj-imdirco  37504  bj-ccinftydisj  37527  wl-dfclab  37910  eldmqsres2  38615  disjdmqscossss  39227  prter2  39327  dihglb2  41788  prjspeclsp  43045  pm11.6  44819  pm11.71  44824  rfcnnnub  45467  eliunxp2  48810  thinccic  49946