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

Definition df-sn 3550
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 3558. (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 3544 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1618 . . . 4  class  x
54, 1wceq 1619 . . 3  wff  x  =  A
65, 3cab 2239 . 2  class  { x  |  x  =  A }
72, 6wceq 1619 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3555  elsn  3559  elsncg  3566  csbsng  3596  rabsn  3601  pw0  3662  iunid  3855  fv2  5373  dfimafn2  5424  fnsnfv  5434  dfiota2  6144  uniabio  6153  snec  6608  infmap2  7728  cf0  7761  cflecard  7763  brdom7disj  8040  brdom6disj  8041  vdwlem6  12907  hashbc0  12926  psrbagsn  16068  ptcmplem2  17579  snclseqg  17630  nmoo0  21199  nmop0  22396  nmfn0  22397  derang0  22871  dfiota3  23636  uvcff  26406  iotain  26784  csbsngVD  27359  lineset  28616
  Copyright terms: Public domain W3C validator