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

Metamath Proof Explorer

Theorem absn

Description: Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 . (Contributed by Andrew Salmon, 30-Jun-2011) (Revised by AV, 24-Aug-2022)

		Ref	Expression
	Assertion	absn	$⊢ \{x \| φ\} = \{Y\} \leftrightarrow \forall x (φ \leftrightarrow x = Y)$

Proof

Step	Hyp	Ref	Expression
1		df-sn	$⊢ \{Y\} = \{x \| x = Y\}$
2	1	eqeq2i	$⊢ \{x \| φ\} = \{Y\} \leftrightarrow \{x \| φ\} = \{x \| x = Y\}$
3		abbib	$⊢ \{x \| φ\} = \{x \| x = Y\} \leftrightarrow \forall x (φ \leftrightarrow x = Y)$
4	2 3	bitri	$⊢ \{x \| φ\} = \{Y\} \leftrightarrow \forall x (φ \leftrightarrow x = Y)$