Theorem aevlem

Lemma for aev and axc16g. Change free and bound variables. Instance of aev. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on [ax-13], along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Reduce axiom usage. (Revised by BJ, 29-Mar-2021.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \forall z \, z = t \)
Proof
l0
cbvaev
\( \vdash \forall x \, x = y' \rightarrow \forall u \, u = y' \)
l1
aevlem0
\( \vdash \forall u \, u = y' \rightarrow \forall x \, x = u \)
l2
cbvaev
\( \vdash \forall x \, x = u \rightarrow \forall t \, t = u \)
aevlem0
\( \vdash \forall t \, t = u \rightarrow \forall z \, z = t \)
4syl l0 l1 l2 _