Theorem speimfw

Specialization, with additional weakening (compared to 19.2) 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, 5-Dec-2017.)

Hypothesis
speimfw.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \neg \forall x \, \neg x = y' \rightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
Proof
df-ex
l1
biimpri _
\( \vdash \neg \forall x \, \neg x = y' \rightarrow \exists x \, x = y' \)
speimfw.2
com12 _
aleximi _
\( \vdash \forall x \, \varphi \rightarrow \exists x \, x = y' \rightarrow \exists x \, \psi \)
syl5com l1 _