Definition df-sn 3715

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 3723. (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 3709	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1401	. . . 4 class 𝑥
5	4, 1	wceq 1402	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2224	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1402	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is used by:  sneq  3720  elsng  3724  csbsng  3770  rabsn  3776  pw0  3862  iunid  4068  dfiota2  5338  uniabio  5348  dfimafn2  5752  fnsnfv  5762  snec  6870  fset0  6949  fngzsum  13708  gzsumvalx  13709  bdcsn  16896