MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sn Unicode version

Definition df-sn 3620
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 3628. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-sn  |-  { A }  =  { x  |  x  =  A }
Distinct variable group:    x, A

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3  class  A
21csn 3614 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1618 . . . 4  class  x
54, 1wceq 1619 . . 3  wff  x  =  A
65, 3cab 2244 . 2  class  { x  |  x  =  A }
72, 6wceq 1619 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3625  elsn  3629  elsncg  3636  csbsng  3666  rabsn  3671  pw0  3736  iunid  3931  fv2  5454  dfimafn2  5506  fnsnfv  5516  dfiota2  6226  uniabio  6235  snec  6690  infmap2  7812  cf0  7845  cflecard  7847  brdom7disj  8124  brdom6disj  8125  vdwlem6  12996  hashbc0  13015  psrbagsn  16199  ptcmplem2  17710  snclseqg  17761  nmoo0  21330  nmop0  22527  nmfn0  22528  derang0  23073  dfiota3  23838  uvcff  26608  iotain  26986  csbsngVD  27802  lineset  29177
  Copyright terms: Public domain W3C validator