euabsn

Description: Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004)

		Ref	Expression
	Assertion	euabsn	$⊢ \exists! x φ \leftrightarrow \exists x \{x \| φ\} = \{x\}$

Step	Hyp	Ref	Expression
1		euabsn2	$⊢ \exists! x φ \leftrightarrow \exists y \{x \| φ\} = \{y\}$
2		nfv	$⊢ Ⅎ y \{x \| φ\} = \{x\}$
3		nfab1	$⊢ \underline{Ⅎ} x \{x \| φ\}$
4	3	nfeq1	$⊢ Ⅎ x \{x \| φ\} = \{y\}$
5		sneq	$⊢ x = y \to \{x\} = \{y\}$
6	5	eqeq2d	$⊢ x = y \to (\{x \| φ\} = \{x\} \leftrightarrow \{x \| φ\} = \{y\})$
7	2 4 6	cbvexv1	$⊢ \exists x \{x \| φ\} = \{x\} \leftrightarrow \exists y \{x \| φ\} = \{y\}$
8	1 7	bitr4i	$⊢ \exists! x φ \leftrightarrow \exists x \{x \| φ\} = \{x\}$

Metamath Proof Explorer