This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 V$
	Assertion	eueqi	$⊢ \exists! x x = A$

Proof

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