Theorem axc16gALT

Alternate proof of axc16g that uses [df-sb] and requires [ax-10], [ax-11], [ax-13]. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \varphi \rightarrow \forall z \, \varphi \)
Proof
l0
aev
\( \vdash \forall x \, x = y' \rightarrow \forall z \, z = x \)
l1
axc16ALT
\( \vdash \forall x \, x = y' \rightarrow \varphi \rightarrow \forall x \, \varphi \)
biidd
dral1 _
biimprd _
\( \vdash \forall z \, z = x \rightarrow \forall x \, \varphi \rightarrow \forall z \, \varphi \)
sylsyld l0 l1 _