Theorem spimevw 2018

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000

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

This theorem is used by:  dtruALT2  5332  zfpair  5383  axprlem3  5387  exneq  5404  fvn0ssdmfun  7074  axnulregtco  37268  onsupmaxb  44240  refimssco  44606  rlimdmafv  48246  rlimdmafv2  48327  elsprel  48556