This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 x x = y \to \forall z z = t$

Proof

Step	Hyp	Ref	Expression
1		cbvaev	$⊢ \forall x x = y \to \forall u u = y$
2		aevlem0	$⊢ \forall u u = y \to \forall x x = u$
3		cbvaev	$⊢ \forall x x = u \to \forall t t = u$
4		aevlem0	$⊢ \forall t t = u \to \forall z z = t$
5	1 2 3 4	4syl	$⊢ \forall x x = y \to \forall z z = t$