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  3167  gencbvex  3507  euxfrw  3692  euxfr  3694  euind  3695  dfdif3OLD  4081  zfpair  5376  opabn0  5513  eliunxp  5801  relop  5814  dmuni  5878  dminss  6126  imainss  6127  cnvresima  6203  rnco  6225  coass  6238  xpco  6262  rnoprab  7494  eloprabga  7498  f11o  7925  frxp  8105  omeu  8549  domen  8933  xpassen  9035  dif1enOLD  9126  enfii  9150  ttrclselem2  9679  kmlem3  10106  cflem  10198  cflemOLD  10199  genpass  10962  ltexprlem4  10992  hasheqf1oi  14316  elwspths2spth  29897  bnj534  34729  bnj906  34920  bnj908  34921  bnj916  34923  bnj983  34941  bnj986  34945  fmla0  35369  fmlasuc0  35371  rexxfr3dALT  35626  dftr6  35738  bj-eeanvw  36701  bj-substw  36710  bj-csbsnlem  36891  bj-clel3gALT  37036  bj-rest10  37076  bj-restuni  37085  bj-imdirco  37178  bj-ccinftydisj  37201  wl-dfclab  37584  eldmqsres2  38276  disjdmqscossss  38795  prter2  38874  dihglb2  41336  prjspeclsp  42600  pm11.6  44381  pm11.71  44386  rfcnnnub  45030  eliunxp2  48322  thinccic  49460