Theorem axc16g

Generalization of axc16. Use the latter when sufficient. This proof only requires, on top of { [ax-1] -- [ax-7] }, Theorem ax12v. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) Remove dependency on [ax-13], along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv. (Revised by Wolf Lammen, 11-Oct-2021.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \varphi \rightarrow \forall z \, \varphi \)
Proof
l0
aevlem
\( \vdash \forall x \, x = y' \rightarrow \forall z \, z = w \)
ax12v
l2
sps _
\( \vdash \forall z \, z = w \rightarrow \varphi \rightarrow \forall z \, (z = w \rightarrow \varphi) \)
pm2.27
al2imi _
\( \vdash \forall z \, z = w \rightarrow \forall z \, (z = w \rightarrow \varphi) \rightarrow \forall z \, \varphi \)
syld l2 _
\( \vdash \forall z \, z = w \rightarrow \varphi \rightarrow \forall z \, \varphi \)
syl l0 _