Definition df-sn 3742

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 3748. (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 3738	. 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  3745  elsn  3749  elsncg  3756  csbsng  3786  rabsn  3791  iunid  4022  1cex  4143  pw0  4161  elp6  4264  unipw1  4326  dfeu2  4334  dfiota2  4341  uniabio  4350  nnc0suc  4413  ltfintrilem1  4466  nnadjoin  4521  tfinnn  4535  nulnnn  4557  phi011lem1  4599  fconstopab  4816  dfimafn2  5368  fnsnfv  5374  snec  5988  map0e  6024