Definition df-sn 3598

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 3606. (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 3592	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1352	. . . 4 class 𝑥
5	4, 1	wceq 1353	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2163	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1353	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3603  elsng  3607  csbsng  3653  rabsn  3659  pw0  3739  iunid  3942  dfiota2  5179  uniabio  5188  dfimafn2  5565  fnsnfv  5575  snec  6595  bdcsn  14592