Theorem equs5aALT

Alternate proof of equs5a. Uses [ax-12] but not [ax-13]. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \exists x \, (x = y \wedge \forall y \, \varphi) \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
Proof
l0
nfa1
ax-12
imp _
exlimi l0 _