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

Metamath Proof Explorer

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

Proof

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