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

Proof

Step	Hyp	Ref	Expression
1		cbvaev	|- ( A. x x = y -> A. u u = y )
2		aevlem0	|- ( A. u u = y -> A. x x = u )
3		cbvaev	|- ( A. x x = u -> A. t t = u )
4		aevlem0	|- ( A. t t = u -> A. z z = t )
5	1 2 3 4	4syl	|- ( A. x x = y -> A. z z = t )