Definition df-sn 3741

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 3747. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-sn	|- {A} = {x | x = A}

Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-sn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csn 3737	. 2 class {A}
3		vx	. . . . 5 setvar x
4	3	cv 1641	. . . 4 class x
5	4, 1	wceq 1642	. . 3 wff x = A
6	5, 3	cab 2339	. 2 class {x | x = A}
7	2, 6	wceq 1642	1 wff {A} = {x | x = A}

This definition is referenced by:  sneq  3744  elsn  3748  elsncg  3755  csbsng  3785  rabsn  3790  iunid  4021  1cex  4142  pw0  4160  elp6  4263  unipw1  4325  dfeu2  4333  dfiota2  4340  uniabio  4349  nnc0suc  4412  ltfintrilem1  4465  nnadjoin  4520  tfinnn  4534  nulnnn  4556  phi011lem1  4598  fconstopab  4815  dfimafn2  5367  fnsnfv  5373  snec  5987  map0e  6023