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	|- ( A. x x = y -> z = t )

Proof

Step	Hyp	Ref	Expression
1		aevlem	|- ( A. x x = y -> A. u u = z )
2		ax6ev	|- E. u u = t
3		ax7	|- ( u = z -> ( u = t -> z = t ) )
4	3	aleximi	|- ( A. u u = z -> ( E. u u = t -> E. u z = t ) )
5	2 4	mpi	|- ( A. u u = z -> E. u z = t )
6		ax5e	|- ( E. u z = t -> z = t )
7	1 5 6	3syl	|- ( A. x x = y -> z = t )