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	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑧 = 𝑡 )

Proof

Step	Hyp	Ref	Expression
1		cbvaev	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑢 𝑢 = 𝑦 )
2		aevlem0	⊢ ( ∀ 𝑢 𝑢 = 𝑦 → ∀ 𝑥 𝑥 = 𝑢 )
3		cbvaev	⊢ ( ∀ 𝑥 𝑥 = 𝑢 → ∀ 𝑡 𝑡 = 𝑢 )
4		aevlem0	⊢ ( ∀ 𝑡 𝑡 = 𝑢 → ∀ 𝑧 𝑧 = 𝑡 )
5	1 2 3 4	4syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑧 = 𝑡 )