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 )