Theorem euequ

Description: There exists a unique set equal to a given set. Special case of eueqi proved using only predicate calculus. The proof needs y = z be free of x . This is ensured by having x and y be distinct. Alternately, a distinctor -. A. x x = y could have been used instead. See eueq and eueqi for classes. (Contributed by Stefan Allan, 4-Dec-2008) (Proof shortened by Wolf Lammen, 8-Sep-2019) Reduce axiom usage. (Revised by Wolf Lammen, 1-Mar-2023)

	Ref	Expression
Assertion	euequ	|- E! x x = y

Proof

Step	Hyp	Ref	Expression
1		ax6ev	|- E. x x = y
2		ax6ev	|- E. z z = y
3		equeuclr	|- ( z = y -> ( x = y -> x = z ) )
4	3	alrimiv	|- ( z = y -> A. x ( x = y -> x = z ) )
5	2 4	eximii	|- E. z A. x ( x = y -> x = z )
6		eu3v	|- ( E! x x = y <-> ( E. x x = y /\ E. z A. x ( x = y -> x = z ) ) )
7	1 5 6	mpbir2an	|- E! x x = y