Definition df-sn 2470

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

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 2467	. 2 class {A}
3		vx	. . . . 5 set x
4	3	cv 991	. . . 4 class x
5	4, 1	wceq 992	. . 3 wff x = A
6	5, 3	cab 1505	. 2 class {x∣x = A}
7	2, 6	wceq 992	1 wff {A} = {x∣x = A}

This definition is referenced by:  sneq 2475  elsn 2479  rabsn 2506  pw0 2532  iunid 2671  moabex 2844  dmsnop 3577  dfimafn2 3873  fnsnfv 3878  fvopab6 3905  oarec 4332  snec 4437  map0e 4483  pw2en 4587  abfii2 4705  abfii4 4707  brdom7disj 4950  brdom6disj 4951  cf0 5060  cflecard 5062  cfom 5066  sqr0 6873  infxpidmlem9 7772  infmap2 7793  subbas 7856  nmo0 8706  nmop0 10189  nmfn0 10190  zrdivrng 10969  subspemp 11060  singempcon 11134  metsstop 11909

Copyright terms: Public domain