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

Definition df-sn 4003
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 4015. (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 4002 . 2  class  { A }
3 vx . . . . 5  setvar  x
43cv 1436 . . . 4  class  x
54, 1wceq 1437 . . 3  wff  x  =  A
65, 3cab 2414 . 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  4012  elsn  4016  elsncg  4025  csbsng  4061  rabsn  4070  pw0  4150  iunid  4357  dfiota2  5566  uniabio  5575  dfimafn2  5931  fnsnfv  5941  suppvalbr  6929  snec  7434  infmap2  8646  cf0  8679  cflecard  8681  brdom7disj  8957  brdom6disj  8958  vdwlem6  14899  hashbc0  14920  symgbas0  16986  psrbagsn  18653  ptcmplem2  20999  snclseqg  21061  nmoo0  26277  nmop0  27474  nmfn0  27475  disjabrex  28031  disjabrexf  28032  pstmfval  28538  hasheuni  28745  derang0  29680  dfiota3  30475  bj-nuliotaALT  31372  poimirlem28  31671  lineset  33011  frege54cor1c  36147  iotain  36404  csbsngVD  36929  dfaimafn2  38057  rnfdmpr  38384  rabeqsn  38870  rabsssn  38871
  Copyright terms: Public domain W3C validator