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

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