Theorem 19.41v 1953

Description: Version of 19.41 2228 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1971. (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 1889	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		ax5e 1915	. . . 4 ⊢ (∃𝑥𝜓 → 𝜓)
3	2	anim2i 617	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	syl 17	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 472	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1920	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 408	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 208	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  19.41vv  1954  19.41vvv  1955  19.41vvvv  1956  19.42v  1957  exdistrv  1959  r19.41v  3188  gencbvex  3535  euxfrw  3717  euxfr  3719  euind  3720  dfdif3  4114  zfpair  5419  opabn0  5553  eliunxp  5837  relop  5850  dmuni  5914  dminss  6152  imainss  6153  cnvresima  6229  rnco  6251  coass  6264  xpco  6288  rnoprab  7514  eloprabga  7518  f11o  7935  frxp  8114  omeu  8587  domen  8959  xpassen  9068  dif1enOLD  9164  enfii  9191  ttrclselem2  9723  kmlem3  10149  cflem  10243  genpass  11006  ltexprlem4  11036  hasheqf1oi  14315  elwspths2spth  29476  bnj534  34036  bnj906  34227  bnj908  34228  bnj916  34230  bnj983  34248  bnj986  34252  fmla0  34659  fmlasuc0  34661  dftr6  35013  bj-eeanvw  35894  bj-substw  35903  bj-csbsnlem  36086  bj-clel3gALT  36232  bj-rest10  36272  bj-restuni  36281  bj-imdirco  36374  bj-ccinftydisj  36397  wl-dfclab  36761  eldmqsres2  37459  disjdmqscossss  37976  prter2  38054  dihglb2  40516  prjspeclsp  41656  pm11.6  43453  pm11.71  43458  rfcnnnub  44022  eliunxp2  47098  thinccic  47769