Definition df-sn 3625

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 3633. (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 3619	. 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  3630  elsng  3634  csbsng  3680  rabsn  3686  pw0  3766  iunid  3969  dfiota2  5217  uniabio  5226  dfimafn2  5607  fnsnfv  5617  snec  6652  fngsum  12974  igsumvalx  12975  bdcsn  15432