Theorem aev

Description: A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006) Remove dependency on ax-11 . (Revised by Wolf Lammen, 7-Sep-2018) Remove dependency on ax-13 , inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019) Remove dependency on ax-12 . (Revised by Wolf Lammen, 19-Mar-2021)

	Ref	Expression
Assertion	aev	$$⊢\forall xx=y\to \forall zt=u$$

Proof

Step	Hyp	Ref	Expression
1		aevlem	$$⊢\forall xx=y\to \forall vv=w$$
2		aeveq	$$⊢\forall vv=w\to t=u$$
3	2	alrimiv	$$⊢\forall vv=w\to \forall zt=u$$
4	1 3	syl	$$⊢\forall xx=y\to \forall zt=u$$