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

Definition df-sn 3999
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 4011. (Contributed by NM, 21-Jun-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 3998 . 2  class  { A }
3 vx . . . . 5  setvar  x
43cv 1436 . . . 4  class  x
54, 1wceq 1437 . . 3  wff  x  =  A
65, 3cab 2407 . 2  class  { x  |  x  =  A }
72, 6wceq 1437 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4008  elsn  4012  elsncg  4021  csbsng  4058  rabsn  4067  pw0  4147  iunid  4354  dfiota2  5566  uniabio  5575  dfimafn2  5931  fnsnfv  5941  suppvalbr  6929  snec  7437  infmap2  8655  cf0  8688  cflecard  8690  brdom7disj  8966  brdom6disj  8967  vdwlem6  14935  hashbc0  14956  symgbas0  17034  psrbagsn  18717  ptcmplem2  21066  snclseqg  21128  nmoo0  26430  nmop0  27637  nmfn0  27638  disjabrex  28194  disjabrexf  28195  pstmfval  28707  hasheuni  28914  derang0  29900  dfiota3  30695  bj-nuliotaALT  31591  poimirlem28  31932  lineset  33272  frege54cor1c  36481  iotain  36738  csbsngVD  37263  dfaimafn2  38538  rnfdmpr  38878  rabeqsn  39733  rabsssn  39734
  Copyright terms: Public domain W3C validator