Definition df-sn 3638

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 3646. (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 3632	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1371	. . . 4 class 𝑥
5	4, 1	wceq 1372	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2190	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1372	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3643  elsng  3647  csbsng  3693  rabsn  3699  pw0  3779  iunid  3982  dfiota2  5232  uniabio  5241  dfimafn2  5627  fnsnfv  5637  snec  6682  fngsum  13162  igsumvalx  13163  bdcsn  15739