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

Proof

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