Definition df-sn 2408

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

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

This definition is referenced by:  sneq 2413  elsn 2417  rabsn 2441  pw0 2464  moabex 2761  dmsnop 3323  dfimafn2 3753  fnsnfv 3758  oarec 4186  snec 4286  map0e 4332  pw2en 4432  abfii2 4542  abfii4 4544  brdom7disj 4784  brdom6disj 4785  cf0 4890  cflecard 4892  cfom 4896  sqr0 6610  infxpidmlem9 7511  infmap2 7531  subbas 7594  nmo0 8396  nmop0 9849  nmfn0 9850

Copyright terms: Public domain