Theorem spimevw 2019

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001

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

This theorem is used by:  dtruALT2  5336  zfpair  5387  axprlem3  5391  exneq  5408  fvn0ssdmfun  7085  axnulregtco  37401  onsupmaxb  44387  refimssco  44753  rlimdmafv  48392  rlimdmafv2  48473  elsprel  48702