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	$$⊢\forall xx=y\to z=t$$

Proof

Step	Hyp	Ref	Expression
1		aevlem	$$⊢\forall xx=y\to \forall uu=z$$
2		ax6ev	$$⊢\exists uu=t$$
3		ax7	$$⊢u=z\to \left(u=t\to z=t\right)$$
4	3	aleximi	$$⊢\forall uu=z\to \left(\exists uu=t\to \exists uz=t\right)$$
5	2 4	mpi	$$⊢\forall uu=z\to \exists uz=t$$
6		ax5e	$$⊢\exists uz=t\to z=t$$
7	1 5 6	3syl	$$⊢\forall xx=y\to z=t$$