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

Definition df-sn 3587
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 3595. (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 3581 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1618 . . . 4  class  x
54, 1wceq 1619 . . 3  wff  x  =  A
65, 3cab 2242 . 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  3592  elsn  3596  elsncg  3603  csbsng  3633  rabsn  3638  pw0  3703  iunid  3898  fv2  5419  dfimafn2  5471  fnsnfv  5481  dfiota2  6191  uniabio  6200  snec  6655  infmap2  7777  cf0  7810  cflecard  7812  brdom7disj  8089  brdom6disj  8090  vdwlem6  12960  hashbc0  12979  psrbagsn  16163  ptcmplem2  17674  snclseqg  17725  nmoo0  21294  nmop0  22491  nmfn0  22492  derang0  23037  dfiota3  23802  uvcff  26572  iotain  26950  csbsngVD  27682  lineset  29057
  Copyright terms: Public domain W3C validator