Definition df-sn 3675

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 3683. (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 3669	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1396	. . . 4 class 𝑥
5	4, 1	wceq 1397	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2217	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1397	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3680  elsng  3684  csbsng  3730  rabsn  3736  pw0  3820  iunid  4026  dfiota2  5287  uniabio  5297  dfimafn2  5695  fnsnfv  5705  snec  6764  fngsum  13470  igsumvalx  13471  bdcsn  16465