Definition df-sn 3715

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 3723. (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 3709	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1401	. . . 4 class 𝑥
5	4, 1	wceq 1402	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2224	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1402	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is used by:  sneq  3720  elsng  3724  csbsng  3770  rabsn  3776  pw0  3862  iunid  4068  dfiota2  5341  uniabio  5351  dfimafn2  5755  fnsnfv  5765  snec  6874  fset0  6953  fngzsum  13767  gzsumvalx  13768  bdcsn  17101