Theorem eueqi

Description: There exists a unique set equal to a given set. Inference associated with euequ . See euequ in the case of a setvar. (Contributed by NM, 5-Apr-1995)

	Ref	Expression
Hypothesis	eueqi.1	$$⊢A\in \mathrm{V}$$
Assertion	eueqi	$$⊢\exists !xx=A$$

Proof

Step	Hyp	Ref	Expression
1		eueqi.1	$$⊢A\in \mathrm{V}$$
2		eueq	$$⊢A\in \mathrm{V}\leftrightarrow \exists !xx=A$$
3	1 2	mpbi	$$⊢\exists !xx=A$$