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

Metamath Proof Explorer

Theorem aev

Description: A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent. (Contributed by NM, 8-Nov-2006) Remove dependency on ax-11 . (Revised by Wolf Lammen, 7-Sep-2018) Remove dependency on ax-13 , inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019) Remove dependency on ax-12 . (Revised by Wolf Lammen, 19-Mar-2021)

		Ref	Expression
	Assertion	aev	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑡 = 𝑢 )

Proof

Step	Hyp	Ref	Expression
1		aevlem	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑣 𝑣 = 𝑤 )
2		aeveq	⊢ ( ∀ 𝑣 𝑣 = 𝑤 → 𝑡 = 𝑢 )
3	2	alrimiv	⊢ ( ∀ 𝑣 𝑣 = 𝑤 → ∀ 𝑧 𝑡 = 𝑢 )
4	1 3	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑡 = 𝑢 )