Theorem spimevw 2015

Description: Existential introduction, using implicit substitution. This is to spimew 2001 what spimvw 2016 is to spimw 2000. Version of spimev 2424 and spimefv 2234 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 1940	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		spimevw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	1, 2	spimew 2001	1 ⊢ (𝜑 → ∃𝑥𝜓)

This proof depends on syntax axioms:   → wi 4  ∃wex 1809

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997

This proof depends on definitions:  df-bi 210  df-ex 1810

This theorem is used by:  dtruALT2  5341  zfpair  5392  axprlem3  5396  exneq  5417  fvn0ssdmfun  7069  axnulregtco  37019  onsupmaxb  43994  refimssco  44361  rlimdmafv  47942  rlimdmafv2  48023  elsprel  48252