Definition df-sn 3595

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

This definition is referenced by:  sneq  3600  elsng  3604  csbsng  3650  rabsn  3656  pw0  3736  iunid  3937  dfiota2  5171  uniabio  5180  dfimafn2  5557  fnsnfv  5567  snec  6586  bdcsn  14182