Theorem spimevw 1999

Description: Existential introduction, using implicit substitution. This is to spimew 1976 what spimvw 2000 is to spimw 1975. Version of spimev 2392 and spimefv 2192 with an additional disjoint variable condition, using only Tarski's FOL axiom schemes. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 17-Mar-2020.)

Hypothesis

Ref	Expression
spimevw.1	⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))

Assertion

Ref	Expression
spimevw	⊢ (𝜑 → ∃𝑥𝜓)

Distinct variable groups:   𝑥,𝑦   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem spimevw

Step	Hyp	Ref	Expression
1		ax-5 1914	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		spimevw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	1, 2	spimew 1976	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  dtruALT2  5368  zfpair  5419  exneq  5435  dtruOLD  5441  fvn0ssdmfun  7074  onsupmaxb  41974  refimssco  42344  rlimdmafv  45872  rlimdmafv2  45953  elsprel  46130