Definition df-sn 3679

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

This definition is referenced by:  sneq  3684  elsng  3688  csbsng  3734  rabsn  3740  pw0  3825  iunid  4031  dfiota2  5294  uniabio  5304  dfimafn2  5704  fnsnfv  5714  snec  6808  fngsum  13551  igsumvalx  13552  bdcsn  16586