Definition df-sn

Description: Define the singleton of a class. Definition 7.1 of Quine p. 48. For convenience, it is well-defined for proper classes, i.e., those that are not elements of _V , see snprc . For an alternate definition see dfsn2 . (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Assertion	df-sn	$$⊢\left\{A\right\}=\left\{x|x=A\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	csn	$$class\left\{A\right\}$$
2		vx	$$setvarx$$
3	2	cv	$$setvarx$$
4	3 0	wceq	$$wffx=A$$
5	4 2	cab	$$class\left\{x|x=A\right\}$$
6	1 5	wceq	$$wff\left\{A\right\}=\left\{x|x=A\right\}$$