Definition df-sn 3629

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 3637. (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 3623	. 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  3634  elsng  3638  csbsng  3684  rabsn  3690  pw0  3770  iunid  3973  dfiota2  5221  uniabio  5230  dfimafn2  5613  fnsnfv  5623  snec  6664  fngsum  13090  igsumvalx  13091  bdcsn  15600