Theorem ax12ev2

Version of ax12v2 rewritten to use an existential quantifier. One direction of sbalex without the universal quantifier, avoiding [ax-10]. (Contributed by SN, 14-Aug-2025.)

Conclusion
\( \vdash \exists x \, (x = y' \wedge \varphi) \rightarrow x = y' \rightarrow \varphi \)
Proof
l0
exnalimn
\( \vdash \exists x \, (x = y' \wedge \varphi) \leftrightarrow \neg \forall x \, (x = y' \rightarrow \neg \varphi) \)
ax12v2
con1d _
\( \vdash x = y' \rightarrow \neg \forall x \, (x = y' \rightarrow \neg \varphi) \rightarrow \varphi \)
biimtrid l0 _
com12 _