Definition df-sn 3697

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 3705. (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 3691	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1397	. . . 4 class 𝑥
5	4, 1	wceq 1398	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2220	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1398	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3702  elsng  3706  csbsng  3752  rabsn  3758  pw0  3843  iunid  4049  dfiota2  5315  uniabio  5325  dfimafn2  5728  fnsnfv  5738  snec  6832  fngsum  13618  igsumvalx  13619  bdcsn  16657