Definition df-sn 3576

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 3584. (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 3570	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1341	. . . 4 class 𝑥
5	4, 1	wceq 1342	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2150	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1342	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3581  elsng  3585  csbsng  3631  rabsn  3637  pw0  3714  iunid  3915  dfiota2  5148  uniabio  5157  dfimafn2  5530  fnsnfv  5539  snec  6553  bdcsn  13587