Theorem spimfw

Specialization, with additional weakening (compared to sp) to allow bundling of \( x \) and \( y' \). Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.)

Hypotheses
spimfw.1
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
spimfw.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \neg \forall x \, \neg x = y' \rightarrow \forall x \, \varphi \rightarrow \psi \)
Proof
spimfw.2
l1
speimfw _
\( \vdash \neg \forall x \, \neg x = y' \rightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
l2
df-ex
\( \vdash \exists x \, \psi \leftrightarrow \neg \forall x \, \neg \psi \)
spimfw.1
con1i _
\( \vdash \neg \forall x \, \neg \psi \rightarrow \psi \)
sylbi l2 _
\( \vdash \exists x \, \psi \rightarrow \psi \)
syl6 l1 _