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) (Revised by BJ, 29-Mar-2021) (Proof shortened by Wolf Lammen, 30-Mar-2021)

	Ref	Expression
Assertion	aevlem0	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑧 = 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		spaev	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
2	1	alrimiv	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 )
3		cbvaev	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑧 = 𝑦 )
4		equeuclr	⊢ ( 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → 𝑧 = 𝑥 ) )
5	4	al2imi	⊢ ( ∀ 𝑧 𝑥 = 𝑦 → ( ∀ 𝑧 𝑧 = 𝑦 → ∀ 𝑧 𝑧 = 𝑥 ) )
6	2 3 5	sylc	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑧 = 𝑥 )