Theorem 19.41v 1949

Description: Version of 19.41 2236 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  3168  gencbvex  3510  euxfrw  3695  euxfr  3697  euind  3698  dfdif3OLD  4084  zfpair  5379  opabn0  5516  eliunxp  5804  relop  5817  dmuni  5881  dminss  6129  imainss  6130  cnvresima  6206  rnco  6228  coass  6241  xpco  6265  rnoprab  7497  eloprabga  7501  f11o  7928  frxp  8108  omeu  8552  domen  8936  xpassen  9040  dif1enOLD  9132  enfii  9156  ttrclselem2  9686  kmlem3  10113  cflem  10205  cflemOLD  10206  genpass  10969  ltexprlem4  10999  hasheqf1oi  14323  elwspths2spth  29904  bnj534  34736  bnj906  34927  bnj908  34928  bnj916  34930  bnj983  34948  bnj986  34952  fmla0  35376  fmlasuc0  35378  rexxfr3dALT  35633  dftr6  35745  bj-eeanvw  36708  bj-substw  36717  bj-csbsnlem  36898  bj-clel3gALT  37043  bj-rest10  37083  bj-restuni  37092  bj-imdirco  37185  bj-ccinftydisj  37208  wl-dfclab  37591  eldmqsres2  38283  disjdmqscossss  38802  prter2  38881  dihglb2  41343  prjspeclsp  42607  pm11.6  44388  pm11.71  44393  rfcnnnub  45037  eliunxp2  48326  thinccic  49464