Theorem spimevw

Existential introduction, using implicit substitution. This is to spimew what spimvw is to spimw. Version of spimev and spimefv 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
spimevw.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \)
Proof
l0
ax-5
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
spimevw.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
spimew l0 _