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  3168  gencbvex  3488  euxfrw  3668  euxfr  3670  euind  3671  dfdif3OLD  4059  zfpair  5358  opabn0  5501  eliunxp  5786  relop  5799  dmuni  5863  dminss  6111  imainss  6112  cnvresima  6188  rnco  6210  rncoOLD  6211  coass  6224  xpco  6247  rnoprab  7465  eloprabga  7469  f11o  7893  frxp  8069  omeu  8513  domen  8901  xpassen  9002  enfii  9113  ttrclselem2  9638  kmlem3  10066  cflem  10158  cflemOLD  10159  genpass  10923  ltexprlem4  10953  hasheqf1oi  14304  elwspths2spth  30053  bnj534  34898  bnj906  35088  bnj908  35089  bnj916  35091  bnj983  35109  bnj986  35113  fmla0  35580  fmlasuc0  35582  rexxfr3dALT  35837  dftr6  35949  bj-eeanvw  37028  bj-substw  37038  bj-csbsnlem  37226  bj-clel3gALT  37371  bj-rest10  37416  bj-restuni  37425  bj-imdirco  37520  bj-ccinftydisj  37543  wl-dfclab  37924  eldmqsres2  38629  disjdmqscossss  39241  prter2  39341  dihglb2  41802  prjspeclsp  43059  pm11.6  44837  pm11.71  44842  rfcnnnub  45485  eliunxp2  48822  thinccic  49958