Theorem equs5eALT

Alternate proof of equs5e. Uses [ax-12] but not [ax-13]. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

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