Definition df-sn 3381

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 3389. (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 3375	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1242	. . . 4 class 𝑥
5	4, 1	wceq 1243	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2026	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1243	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3386  elsng  3390  csbsng  3431  rabsn  3437  pw0  3511  iunid  3712  dfiota2  4868  uniabio  4877  dfimafn2  5223  fnsnfv  5232  snec  6167  bdcsn  9990