Definition df-sn 3599

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 3607. (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 3593	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1352	. . . 4 class 𝑥
5	4, 1	wceq 1353	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2163	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1353	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3604  elsng  3608  csbsng  3654  rabsn  3660  pw0  3740  iunid  3943  dfiota2  5180  uniabio  5189  dfimafn2  5566  fnsnfv  5576  snec  6596  bdcsn  14625