Theorem axc16

Proof of older axiom [ax-c16]. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \varphi \rightarrow \forall x \, \varphi \)
Proof
l0
aevlem
\( \vdash \forall x \, x = y' \rightarrow \forall v \, v = w \)
l1
aevlem
\( \vdash \forall v \, v = w \rightarrow \forall x \, x = w \)
l2
syl l0 _
l3
ax12v
l4
sps _
\( \vdash \forall x \, x = w \rightarrow \varphi \rightarrow \forall x \, (x = w \rightarrow \varphi) \)
l5
pm2.27
l6
al2imi _
\( \vdash \forall x \, x = w \rightarrow \forall x \, (x = w \rightarrow \varphi) \rightarrow \forall x \, \varphi \)
l7
syld l4 _
l8
syl l2 _