Theorem 19.41v 1956

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

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  19.41vv  1957  19.41vvv  1958  19.41vvvv  1959  19.42v  1960  exdistrv  1962  r19.41v  3170  gencbvex  3490  euxfrw  3669  euxfr  3671  euind  3672  dfdif3OLD  4056  zfpair  5357  opabn0  5502  eliunxp  5786  relop  5799  dmuni  5863  dminss  6111  imainss  6112  cnvresima  6188  rnco  6210  rncoOLD  6211  coass  6224  xpco  6247  rnoprab  7468  eloprabga  7472  f11o  7896  frxp  8073  omeu  8517  domen  8905  xpassen  9006  enfii  9117  ttrclselem2  9645  kmlem3  10073  cflem  10165  cflemOLD  10166  genpass  10930  ltexprlem4  10960  hasheqf1oi  14311  elwspths2spth  30063  bnj534  34929  bnj906  35119  bnj908  35120  bnj916  35122  bnj983  35140  bnj986  35144  fmla0  35617  fmlasuc0  35619  rexxfr3dALT  35874  dftr6  35986  bj-eeanvw  37065  bj-substw  37075  bj-csbsnlem  37263  bj-clel3gALT  37408  bj-rest10  37453  bj-restuni  37462  bj-imdirco  37557  bj-ccinftydisj  37580  wl-dfclab  37963  eldmqsres2  38668  disjdmqscossss  39280  prter2  39380  dihglb2  41841  prjspeclsp  43069  pm11.6  44843  pm11.71  44848  rfcnnnub  45491  eliunxp2  48832  thinccic  49968