Definition df-sn 3404

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 3412. (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 3398	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1283	. . . 4 class 𝑥
5	4, 1	wceq 1284	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2067	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1284	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3409  elsng  3413  csbsng  3453  rabsn  3459  pw0  3532  iunid  3733  dfiota2  4888  uniabio  4897  dfimafn2  5244  fnsnfv  5253  snec  6190  bdcsn  10661