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

Definition df-sn 3659
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 3667. (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 3653 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1631 . . . 4  class  x
54, 1wceq 1632 . . 3  wff  x  =  A
65, 3cab 2282 . 2  class  { x  |  x  =  A }
72, 6wceq 1632 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3664  elsn  3668  elsncg  3675  csbsng  3705  rabsn  3710  pw0  3778  iunid  3973  dfiota2  5236  uniabio  5245  dfimafn2  5588  fnsnfv  5598  snec  6738  infmap2  7860  cf0  7893  cflecard  7895  brdom7disj  8172  brdom6disj  8173  vdwlem6  13049  hashbc0  13068  psrbagsn  16252  ptcmplem2  17763  snclseqg  17814  nmoo0  21385  nmop0  22582  nmfn0  22583  disjabrex  23374  disjabrexf  23375  hasheuni  23468  derang0  23715  dfiota3  24533  uvcff  27343  iotain  27720  dfaimafn2  28134  csbsngVD  28985  lineset  30549
  Copyright terms: Public domain W3C validator