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

Definition df-singles 24404
Description: Define the class of all singletons. See elsingles 24457 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 24382 . 2  class  Singletons
2 csingle 24381 . . 3  class Singleton
32crn 4690 . 2  class  ran Singleton
41, 3wceq 1623 1  wff  Singletons  =  ran Singleton
Colors of variables: wff set class
This definition is referenced by:  elsingles  24457
  Copyright terms: Public domain W3C validator