Theorem spimew

Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Wolf Lammen, 22-Oct-2023.)

Hypotheses
spimew.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
spimew.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \)
Proof
l0
ax6v
\( \vdash \neg \forall x \, \neg x = y' \)
l1
spimew.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
spimew.2
speimfw _
\( \vdash \neg \forall x \, \neg x = y' \rightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
mpsyl l0 l1 _