Theorem spimev

Distinct-variable version of spime. (Contributed by NM, 10-Jan-1993.) Usage of this theorem is discouraged because it depends on [ax-13]. Use spimevw instead. (New usage is discouraged.)

Hypothesis
spimev.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \)
Proof
l0
nfv
\( \vdash \Finv x \, \varphi \)
spimev.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
spime l0 _