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	$$⊢\left\{x|\phi \right\}=\left\{Y\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow x=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-sn	$$⊢\left\{Y\right\}=\left\{x|x=Y\right\}$$
2	1	eqeq2i	$$⊢\left\{x|\phi \right\}=\left\{Y\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{x|x=Y\right\}$$
3		abbi	$$⊢\forall x\left(\phi \leftrightarrow x=Y\right)\leftrightarrow \left\{x|\phi \right\}=\left\{x|x=Y\right\}$$
4	2 3	bitr4i	$$⊢\left\{x|\phi \right\}=\left\{Y\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow x=Y\right)$$