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	$$⊢\exists !xx=y$$

Proof

Step	Hyp	Ref	Expression
1		ax6ev	$$⊢\exists xx=y$$
2		ax6ev	$$⊢\exists zz=y$$
3		equeuclr	$$⊢z=y\to \left(x=y\to x=z\right)$$
4	3	alrimiv	$$⊢z=y\to \forall x\left(x=y\to x=z\right)$$
5	2 4	eximii	$$⊢\exists z\forall x\left(x=y\to x=z\right)$$
6		eu3v	$$⊢\exists !xx=y\leftrightarrow \left(\exists xx=y\wedge \exists z\forall x\left(x=y\to x=z\right)\right)$$
7	1 5 6	mpbir2an	$$⊢\exists !xx=y$$