Definition df-sn 3644

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 3652. (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 3638	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1372	. . . 4 class 𝑥
5	4, 1	wceq 1373	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2192	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1373	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3649  elsng  3653  csbsng  3699  rabsn  3705  pw0  3786  iunid  3992  dfiota2  5247  uniabio  5256  dfimafn2  5646  fnsnfv  5656  snec  6701  fngsum  13305  igsumvalx  13306  bdcsn  15975