Definition df-sn 3480

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 3488. (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 3474	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1298	. . . 4 class 𝑥
5	4, 1	wceq 1299	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2086	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1299	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3485  elsng  3489  csbsng  3531  rabsn  3537  pw0  3614  iunid  3815  dfiota2  5025  uniabio  5034  dfimafn2  5403  fnsnfv  5412  snec  6420  bdcsn  12649