This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) 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)

Ref Expression
Assertion aevlem0 ⊢ ∀ x x = y → ∀ z z = x

Proof

Step Hyp Ref Expression
1 spaev ⊢ ∀ x x = y → x = y
2 1 alrimiv ⊢ ∀ x x = y → ∀ z x = y
3 cbvaev ⊢ ∀ x x = y → ∀ z z = y
4 equeuclr ⊢ x = y → z = y → z = x
5 4 al2imi ⊢ ∀ z x = y → ∀ z z = y → ∀ z z = x
6 2 3 5 sylc ⊢ ∀ x x = y → ∀ z z = x