Definition df-sn 3672

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 3680. (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 3666	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1394	. . . 4 class 𝑥
5	4, 1	wceq 1395	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2215	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1395	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3677  elsng  3681  csbsng  3727  rabsn  3733  pw0  3815  iunid  4021  dfiota2  5279  uniabio  5289  dfimafn2  5685  fnsnfv  5695  snec  6751  fngsum  13436  igsumvalx  13437  bdcsn  16288