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

Definition df-sn 3647
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 3655. (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 3641 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1622 . . . 4  class  x
54, 1wceq 1623 . . 3  wff  x  =  A
65, 3cab 2270 . 2  class  { x  |  x  =  A }
72, 6wceq 1623 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3652  elsn  3656  elsncg  3663  csbsng  3693  rabsn  3698  pw0  3763  iunid  3958  fv2  5482  dfimafn2  5534  fnsnfv  5544  dfiota2  6254  uniabio  6263  snec  6718  infmap2  7840  cf0  7873  cflecard  7875  brdom7disj  8152  brdom6disj  8153  vdwlem6  13029  hashbc0  13048  psrbagsn  16232  ptcmplem2  17743  snclseqg  17794  nmoo0  21363  nmop0  22562  nmfn0  22563  derang0  23107  dfiota3  23872  uvcff  26651  iotain  27028  dfaimafn2  27419  csbsngVD  27949  lineset  29206
  Copyright terms: Public domain W3C validator