Theorem aevlem0

Lemma for aevlem. Instance of aev. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on [ax-12]. (Revised by Wolf Lammen, 14-Mar-2021.) Extract from proof of a former lemma for axc11n and add DV condition to reduce axiom usage. (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \forall z \, z = x \)
Proof
spaev
l1
alrimiv _
\( \vdash \forall x \, x = y' \rightarrow \forall z \, x = y' \)
l2
cbvaev
\( \vdash \forall x \, x = y' \rightarrow \forall z \, z = y' \)
equeuclr
al2imi _
\( \vdash \forall z \, x = y' \rightarrow \forall z \, z = y' \rightarrow \forall z \, z = x \)
sylc l1 l2 _