Definition df-sn 3533

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 3541. (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 3527	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1330	. . . 4 class 𝑥
5	4, 1	wceq 1331	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2125	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1331	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3538  elsng  3542  csbsng  3584  rabsn  3590  pw0  3667  iunid  3868  dfiota2  5089  uniabio  5098  dfimafn2  5471  fnsnfv  5480  snec  6490  bdcsn  13068