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

Metamath Proof Explorer

Theorem absneu

Description: Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006)

		Ref	Expression
	Assertion	absneu	$⊢ (A \in V \land \{x \| φ\} = \{A\}) \to \exists! x φ$

Step	Hyp	Ref	Expression
1		sneq	$⊢ y = A \to \{y\} = \{A\}$
2	1	eqeq2d	$⊢ y = A \to (\{x \| φ\} = \{y\} \leftrightarrow \{x \| φ\} = \{A\})$
3	2	spcegv	$⊢ A \in V \to (\{x \| φ\} = \{A\} \to \exists y \{x \| φ\} = \{y\})$
4	3	imp	$⊢ (A \in V \land \{x \| φ\} = \{A\}) \to \exists y \{x \| φ\} = \{y\}$
5		euabsn2	$⊢ \exists! x φ \leftrightarrow \exists y \{x \| φ\} = \{y\}$
6	4 5	sylibr	$⊢ (A \in V \land \{x \| φ\} = \{A\}) \to \exists! x φ$