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) Reduce axiom usage. (Revised by BJ, 29-Mar-2021)

	Ref	Expression
Assertion	aevlem	$$⊢\forall xx=y\to \forall zz=t$$

Proof

Step	Hyp	Ref	Expression
1		cbvaev	$$⊢\forall xx=y\to \forall uu=y$$
2		aevlem0	$$⊢\forall uu=y\to \forall xx=u$$
3		cbvaev	$$⊢\forall xx=u\to \forall tt=u$$
4		aevlem0	$$⊢\forall tt=u\to \forall zz=t$$
5	1 2 3 4	4syl	$$⊢\forall xx=y\to \forall zz=t$$