Definition df-sn 3624

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 3632. (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 3618	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1363	. . . 4 class 𝑥
5	4, 1	wceq 1364	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2179	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1364	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3629  elsng  3633  csbsng  3679  rabsn  3685  pw0  3765  iunid  3968  dfiota2  5216  uniabio  5225  dfimafn2  5606  fnsnfv  5616  snec  6650  fngsum  12971  igsumvalx  12972  bdcsn  15362