Definition df-sn 3714

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 3722. (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 3708	. 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 referenced by:  sneq  3719  elsng  3723  csbsng  3769  rabsn  3775  pw0  3860  iunid  4066  dfiota2  5336  uniabio  5346  dfimafn2  5749  fnsnfv  5759  snec  6863  fset0  6942  fngzsum  13688  gzsumvalx  13689  bdcsn  16813