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	$$⊢\forall xx=y\to \forall zz=x$$

Proof

Step	Hyp	Ref	Expression
1		spaev	$$⊢\forall xx=y\to x=y$$
2	1	alrimiv	$$⊢\forall xx=y\to \forall zx=y$$
3		cbvaev	$$⊢\forall xx=y\to \forall zz=y$$
4		equeuclr	$$⊢x=y\to \left(z=y\to z=x\right)$$
5	4	al2imi	$$⊢\forall zx=y\to \left(\forall zz=y\to \forall zz=x\right)$$
6	2 3 5	sylc	$$⊢\forall xx=y\to \forall zz=x$$