# Metamath Proof Explorer

## Theorem aevlem

Description: 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) (Revised by BJ, 29-Mar-2021)

Ref Expression
Assertion aevlem ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{z}={t}$

### Proof

Step Hyp Ref Expression
1 cbvaev ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}$
2 aevlem0 ${⊢}\forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{x}={u}$
3 cbvaev ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={u}\to \forall {t}\phantom{\rule{.4em}{0ex}}{t}={u}$
4 aevlem0 ${⊢}\forall {t}\phantom{\rule{.4em}{0ex}}{t}={u}\to \forall {z}\phantom{\rule{.4em}{0ex}}{z}={t}$
5 1 2 3 4 4syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{z}={t}$