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 
|- ( A. x x = y -> A. z z = x )

Proof

Step Hyp Ref Expression
1 spaev 
 |-  ( A. x x = y -> x = y )
2 1 alrimiv 
 |-  ( A. x x = y -> A. z x = y )
3 cbvaev 
 |-  ( A. x x = y -> A. z z = y )
4 equeuclr 
 |-  ( x = y -> ( z = y -> z = x ) )
5 4 al2imi 
 |-  ( A. z x = y -> ( A. z z = y -> A. z z = x ) )
6 2 3 5 sylc 
 |-  ( A. x x = y -> A. z z = x )