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

Definition df-sn 3646
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 3654. (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 3640 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1622 . . . 4  class  x
54, 1wceq 1623 . . 3  wff  x  =  A
65, 3cab 2269 . 2  class  { x  |  x  =  A }
72, 6wceq 1623 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3651  elsn  3655  elsncg  3662  csbsng  3692  rabsn  3697  pw0  3762  iunid  3957  dfiota2  5220  uniabio  5229  dfimafn2  5572  fnsnfv  5582  snec  6722  infmap2  7844  cf0  7877  cflecard  7879  brdom7disj  8156  brdom6disj  8157  vdwlem6  13033  hashbc0  13052  psrbagsn  16236  ptcmplem2  17747  snclseqg  17798  nmoo0  21369  nmop0  22566  nmfn0  22567  disjabrex  23359  disjabrexf  23360  hasheuni  23453  derang0  23700  dfiota3  24462  uvcff  27240  iotain  27617  dfaimafn2  28028  csbsngVD  28669  lineset  29927
  Copyright terms: Public domain W3C validator