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  3189  gencbvex  3541  euxfrw  3727  euxfr  3729  euind  3730  dfdif3OLD  4118  zfpair  5421  opabn0  5558  eliunxp  5848  relop  5861  dmuni  5925  dminss  6173  imainss  6174  cnvresima  6250  rnco  6272  coass  6285  xpco  6309  rnoprab  7538  eloprabga  7542  f11o  7971  frxp  8151  omeu  8623  domen  9002  xpassen  9106  dif1enOLD  9202  enfii  9226  ttrclselem2  9766  kmlem3  10193  cflem  10285  cflemOLD  10286  genpass  11049  ltexprlem4  11079  hasheqf1oi  14390  elwspths2spth  29987  bnj534  34753  bnj906  34944  bnj908  34945  bnj916  34947  bnj983  34965  bnj986  34969  fmla0  35387  fmlasuc0  35389  rexxfr3dALT  35644  dftr6  35751  bj-eeanvw  36714  bj-substw  36723  bj-csbsnlem  36904  bj-clel3gALT  37049  bj-rest10  37089  bj-restuni  37098  bj-imdirco  37191  bj-ccinftydisj  37214  wl-dfclab  37597  eldmqsres2  38289  disjdmqscossss  38804  prter2  38882  dihglb2  41344  prjspeclsp  42622  pm11.6  44411  pm11.71  44416  rfcnnnub  45041  eliunxp2  48250  thinccic  49118