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

Definition df-sn 3765
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 3773. (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 3759 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1648 . . . 4  class  x
54, 1wceq 1649 . . 3  wff  x  =  A
65, 3cab 2375 . 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  3770  elsn  3774  elsncg  3781  csbsng  3812  rabsn  3818  pw0  3890  iunid  4089  dfiota2  5361  uniabio  5370  dfimafn2  5717  fnsnfv  5727  snec  6905  infmap2  8033  cf0  8066  cflecard  8068  brdom7disj  8344  brdom6disj  8345  vdwlem6  13283  hashbc0  13302  psrbagsn  16484  ptcmplem2  18007  snclseqg  18068  nmoo0  22142  nmop0  23339  nmfn0  23340  disjabrex  23870  disjabrexf  23871  hasheuni  24273  derang0  24636  dfiota3  25488  uvcff  26911  iotain  27288  dfaimafn2  27701  csbsngVD  28348  lineset  29854
  Copyright terms: Public domain W3C validator