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

Definition df-sn 4015
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 4027. (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 4014 . 2  class  { A }
3 vx . . . . 5  setvar  x
43cv 1382 . . . 4  class  x
54, 1wceq 1383 . . 3  wff  x  =  A
65, 3cab 2428 . 2  class  { x  |  x  =  A }
72, 6wceq 1383 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4024  elsn  4028  elsncg  4037  csbsng  4073  rabsn  4082  pw0  4162  iunid  4370  dfiota2  5542  uniabio  5551  dfimafn2  5908  fnsnfv  5918  suppvalbr  6907  snec  7376  infmap2  8601  cf0  8634  cflecard  8636  brdom7disj  8912  brdom6disj  8913  vdwlem6  14486  hashbc0  14505  symgbas0  16398  psrbagsn  18139  ptcmplem2  20531  snclseqg  20592  nmoo0  25684  nmop0  26883  nmfn0  26884  disjabrex  27421  disjabrexf  27422  pstmfval  27853  hasheuni  28069  derang0  28591  dfiota3  29549  iotain  31278  dfaimafn2  32205  rnfdmpr  32262  rabeqsn  32787  rabsssn  32788  csbsngVD  33561  bj-nuliotaALT  34470  lineset  35337  frege54cor1c  37746
  Copyright terms: Public domain W3C validator