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 33331
Description: Define the class of all singletons. See elsingles 33386 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 33307 . 2 class Singletons
2 csingle 33306 . . 3 class Singleton
32crn 5529 . 2 class ran Singleton
41, 3wceq 1538 1 wff Singletons = ran Singleton
Colors of variables: wff setvar class
This definition is referenced by:  elsingles  33386
  Copyright terms: Public domain W3C validator