Definition df-sn 1811

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, although it is not very meaningful in this case. For an alternate definition see dfsn2 1819.

Assertion

Ref	Expression
df-sn	⊢ {A} = {x∣x = A}

Distinct variable group(s):   x,A

Detailed syntax breakdown of Definition df-sn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csn 1808	. 2 class {A}
3		vx	. . . . 5 set x
4	3	cv 1089	. . . 4 class x
5	4, 1	wceq 1091	. . 3 wff x = A
6	5, 3	cab 1090	. 2 class {x∣x = A}
7	2, 6	wceq 1091	1 wff {A} = {x∣x = A}

This definition is referenced by:  sneq 1816  elsn 1820  moabex 1868  pw0 1882  dmsnop 2547  fnsnfv 2861  snec 3232  map0e 3266  pw2en 3348  cf0 3705  cflecard 3707  cfom 3710  sqr0 4730  infxpidmlem9 4941  infmap2 4953

metamath.org