Definition df-sn 3274

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

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 3270	. 2 class {A}
3		vx	. . . . 5 set x
4	3	cv 1614	. . . 4 class x
5	4, 1	wceq 1615	. . 3 wff x = A
6	5, 3	cab 2157	. 2 class {x | x = A}
7	2, 6	wceq 1615	1 wff {A} = {x | x = A}

This definition is referenced by:  sneq 3279  elsn 3283  elsncg 3289  csbsng 3311  rabsn 3316  pw0 3357  iunid 3513  moabex 3708  dfimafn2 4846  fnsnfv 4851  fvopab6 4882  dfiota2 5260  uniabio 5269  oarec 5447  snec 5559  map0e 5605  pw2en 5714  abfii2 5918  abfii4 5920  cf0 6337  cflecard 6339  cfom 6344  brdom7disj 6454  brdom6disj 6455  cfomOLD 6525  sqr0 8422  infxpidmlem9OLD 9359  infmap2 9380  subbas 9915  nmo0 10814  zrdivrng 11414  nmop0 12537  nmfn0 12538  subspemp 15926  singempcon 16004  idtrgrp 16017  pi1bval 17173  iotain 17466  csbsngVD 17812  lineset 18443

Copyright terms: Public domain