Theorem aev

A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent. (Contributed by NM, 8-Nov-2006.) Remove dependency on [ax-11]. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on [ax-13], inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on [ax-12]. (Revised by Wolf Lammen, 19-Mar-2021.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \forall z \, t' = u' \)
Proof
l0
aevlem
\( \vdash \forall x \, x = y' \rightarrow \forall v \, v = w \)
aeveq
alrimiv _
\( \vdash \forall v \, v = w \rightarrow \forall z \, t' = u' \)
syl l0 _