Definition df-sn 3589

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 3597. (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 3583	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1347	. . . 4 class 𝑥
5	4, 1	wceq 1348	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2156	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1348	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3594  elsng  3598  csbsng  3644  rabsn  3650  pw0  3727  iunid  3928  dfiota2  5161  uniabio  5170  dfimafn2  5546  fnsnfv  5555  snec  6574  bdcsn  13905