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 e. _V
Assertion	eueqi	|- E! x x = A

Proof

Step	Hyp	Ref	Expression
1		eueqi.1	|- A e. _V
2		eueq	|- ( A e. _V <-> E! x x = A )
3	1 2	mpbi	|- E! x x = A