Definition df-sn 2412

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

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 2409	. 2 class {A}
3		vx	. . . . 5 set x
4	3	cv 955	. . . 4 class x
5	4, 1	wceq 956	. . 3 wff x = A
6	5, 3	cab 1463	. 2 class {x | x = A}
7	2, 6	wceq 956	1 wff {A} = {x | x = A}

This definition is referenced by:  sneq 2417  elsn 2421  rabsn 2445  pw0 2468  moabex 2766  dmsnop 3328  dfimafn2 3762  fnsnfv 3767  oarec 4196  snec 4296  map0e 4342  pw2en 4446  abfii2OLD 4562  abfii4OLD 4564  brdom7disj 4804  brdom6disj 4805  cf0 4910  cflecard 4912  cfom 4916  sqr0 6672  infxpidmlem9 7560  infmap2 7581  subbasOLD 7644  nmo0 8451  nmop0 9910  nmfn0 9911

Copyright terms: Public domain