Definition df-sn 3700

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 3708. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-sn	⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-sn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	csn 3694	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1397	. . . 4 class 𝑥
5	4, 1	wceq 1398	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2220	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1398	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3705  elsng  3709  csbsng  3755  rabsn  3761  pw0  3846  iunid  4052  dfiota2  5318  uniabio  5328  dfimafn2  5731  fnsnfv  5741  snec  6843  fngsum  13651  igsumvalx  13652  bdcsn  16766