Theorem spime

Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. See spimew and spimevw for weaker versions requiring fewer axioms. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) Usage of this theorem is discouraged because it depends on [ax-13]. Use spimefv instead. (New usage is discouraged.)

Hypotheses
spime.1
\( \vdash \Finv x \, \varphi \)
spime.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \)
Proof
spime.1
l1
a1i _
\( \vdash \top \rightarrow \Finv x \, \varphi \)
spime.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
spimed l1 _
mptru _