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  3814  iunid  4020  dfiota2  5278  uniabio  5288  dfimafn2  5682  fnsnfv  5692  snec  6741  fngsum  13416  igsumvalx  13417  bdcsn  16191