Definition df-sn 3582

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 3590. (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 3576	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1342	. . . 4 class 𝑥
5	4, 1	wceq 1343	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2151	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1343	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3587  elsng  3591  csbsng  3637  rabsn  3643  pw0  3720  iunid  3921  dfiota2  5154  uniabio  5163  dfimafn2  5536  fnsnfv  5545  snec  6562  bdcsn  13752