# Metamath Proof Explorer

## Theorem aevlem0

Description: 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) (Revised by BJ, 29-Mar-2021) (Proof shortened by Wolf Lammen, 30-Mar-2021)

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

### Proof

Step Hyp Ref Expression
1 spaev ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to {x}={y}$
2 1 alrimiv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{x}={y}$
3 cbvaev ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
4 equeuclr ${⊢}{x}={y}\to \left({z}={y}\to {z}={x}\right)$
5 4 al2imi ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\right)$
6 2 3 5 sylc ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}$