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

Metamath Proof Explorer

Theorem eusn

Description: Two ways to express " A is a singleton". (Contributed by NM, 30-Oct-2010)

		Ref	Expression
	Assertion	eusn	$⊢ \exists! x x \in A \leftrightarrow \exists x A = \{x\}$

Step	Hyp	Ref	Expression
1		euabsn	$⊢ \exists! x x \in A \leftrightarrow \exists x \{x \| x \in A\} = \{x\}$
2		abid2	$⊢ \{x \| x \in A\} = A$
3	2	eqeq1i	$⊢ \{x \| x \in A\} = \{x\} \leftrightarrow A = \{x\}$
4	3	exbii	$⊢ \exists x \{x \| x \in A\} = \{x\} \leftrightarrow \exists x A = \{x\}$
5	1 4	bitri	$⊢ \exists! x x \in A \leftrightarrow \exists x A = \{x\}$