Theorem spei

Inference from existential specialization, using implicit substitution. Remove a distinct variable constraint. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker speiv if possible. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.)

Hypotheses
spei.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
spei.2
\( \vdash \psi \)
Conclusion
\( \vdash \exists x \, \varphi \)
Proof
l0
ax6e
\( \vdash \exists x \, x = y' \)
l1
spei.2
\( \vdash \psi \)
spei.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
mpbiri l1 _
\( \vdash x = y' \rightarrow \varphi \)
eximii l0 _