Definition df-sn 2402

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 2410.

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 2399	. 2 class {A}
3		vx	. . . . 5 set x
4	3	cv 952	. . . 4 class x
5	4, 1	wceq 953	. . 3 wff x = A
6	5, 3	cab 1456	. 2 class {x | x = A}
7	2, 6	wceq 953	1 wff {A} = {x | x = A}

This definition is referenced by:  sneq 2407  elsn 2411  rabsn 2435  pw0 2459  moabex 2756  dmsnop 3317  dfimafn2 3747  fnsnfv 3752  oarec 4180  snec 4280  map0e 4326  pw2en 4426  abfii2 4536  abfii4 4538  brdom7disj 4776  brdom6disj 4777  cf0 4882  cflecard 4884  cfom 4888  sqr0 6602  infxpidmlem9 7503  infmap2 7523  subbas 7586  nmo0 8383  nmop0 9826  nmfn0 9827

Copyright terms: Public domain