Definition df-sn 3628

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 3636. (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 3622	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1363	. . . 4 class 𝑥
5	4, 1	wceq 1364	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2182	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1364	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  3633  elsng  3637  csbsng  3683  rabsn  3689  pw0  3769  iunid  3972  dfiota2  5220  uniabio  5229  dfimafn2  5610  fnsnfv  5620  snec  6655  fngsum  13031  igsumvalx  13032  bdcsn  15516