Theorem aeveq

Description: The antecedent A. x x = y with a disjoint variable condition (typical of a one-object universe) forces equality of everything. (Contributed by Wolf Lammen, 19-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		aevlem	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑢 𝑢 = 𝑧 )
2		ax6ev	⊢ ∃ 𝑢 𝑢 = 𝑡
3		ax7	⊢ ( 𝑢 = 𝑧 → ( 𝑢 = 𝑡 → 𝑧 = 𝑡 ) )
4	3	aleximi	⊢ ( ∀ 𝑢 𝑢 = 𝑧 → ( ∃ 𝑢 𝑢 = 𝑡 → ∃ 𝑢 𝑧 = 𝑡 ) )
5	2 4	mpi	⊢ ( ∀ 𝑢 𝑢 = 𝑧 → ∃ 𝑢 𝑧 = 𝑡 )
6		ax5e	⊢ ( ∃ 𝑢 𝑧 = 𝑡 → 𝑧 = 𝑡 )
7	1 5 6	3syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑧 = 𝑡 )