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

Definition df-sn 3784
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 3792. (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 3778 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1648 . . . 4  class  x
54, 1wceq 1649 . . 3  wff  x  =  A
65, 3cab 2394 . 2  class  { x  |  x  =  A }
72, 6wceq 1649 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3789  elsn  3793  elsncg  3800  csbsng  3831  rabsn  3837  pw0  3909  iunid  4110  dfiota2  5382  uniabio  5391  dfimafn2  5739  fnsnfv  5749  snec  6930  infmap2  8058  cf0  8091  cflecard  8093  brdom7disj  8369  brdom6disj  8370  vdwlem6  13313  hashbc0  13332  psrbagsn  16514  ptcmplem2  18041  snclseqg  18102  nmoo0  22249  nmop0  23446  nmfn0  23447  disjabrex  23981  disjabrexf  23982  pstmfval  24248  hasheuni  24432  derang0  24812  dfiota3  25680  uvcff  27112  iotain  27489  dfaimafn2  27901  rnfdmpr  27968  csbsngVD  28718  lineset  30224
  Copyright terms: Public domain W3C validator