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

Definition df-sn 4023
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 4035. (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 4022 . 2  class  { A }
3 vx . . . . 5  setvar  x
43cv 1373 . . . 4  class  x
54, 1wceq 1374 . . 3  wff  x  =  A
65, 3cab 2447 . 2  class  { x  |  x  =  A }
72, 6wceq 1374 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4032  elsn  4036  elsncg  4045  csbsng  4081  rabsn  4089  pw0  4169  iunid  4375  dfiota2  5545  uniabio  5554  dfimafn2  5910  fnsnfv  5920  suppvalbr  6897  snec  7366  infmap2  8589  cf0  8622  cflecard  8624  brdom7disj  8900  brdom6disj  8901  vdwlem6  14354  hashbc0  14373  symgbas0  16209  psrbagsn  17926  ptcmplem2  20283  snclseqg  20344  nmoo0  25370  nmop0  26569  nmfn0  26570  disjabrex  27104  disjabrexf  27105  pstmfval  27499  hasheuni  27719  derang0  28241  dfiota3  29138  iotain  30859  dfaimafn2  31675  rnfdmpr  31734  rabeqsn  31860  rabsssn  31861  csbsngVD  32650  bj-nuliotaALT  33545  lineset  34411  frege54cor1c  36784
  Copyright terms: Public domain W3C validator