Theorem axc16ALT

Alternate proof of axc16, shorter but requiring [ax-10], [ax-11], [ax-13] and using [df-nf] and [df-sb]. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \varphi \rightarrow \forall x \, \varphi \)
Proof
l0
sbequ12
\( \vdash x = z \rightarrow (\varphi \leftrightarrow [ z / x ] \, \varphi) \)
ax-5
hbsb3 _
\( \vdash [ z / x ] \, \varphi \rightarrow \forall x \, [ z / x ] \, \varphi \)
axc16i l0 _