Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-singles Structured version   Visualization version   GIF version

Definition df-singles 32297
Description: Define the class of all singletons. See elsingles 32352 for membership. (Contributed by Scott Fenton, 19-Feb-2013.)
Assertion
Ref Expression
df-singles Singletons = ran Singleton

Detailed syntax breakdown of Definition df-singles
StepHypRef Expression
1 csingles 32273 . 2 class Singletons
2 csingle 32272 . . 3 class Singleton
32crn 5267 . 2 class ran Singleton
41, 3wceq 1632 1 wff Singletons = ran Singleton
Colors of variables: wff setvar class
This definition is referenced by:  elsingles  32352
  Copyright terms: Public domain W3C validator