Definition df-sn 3673

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 3681. (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 3667	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1394	. . . 4 class 𝑥
5	4, 1	wceq 1395	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2215	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1395	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3678  elsng  3682  csbsng  3728  rabsn  3734  pw0  3818  iunid  4024  dfiota2  5285  uniabio  5295  dfimafn2  5691  fnsnfv  5701  snec  6760  fngsum  13461  igsumvalx  13462  bdcsn  16401