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 35368
Description: Define the class of all singletons. See elsingles 35423 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 35344 . 2 class Singletons
2 csingle 35343 . . 3 class Singleton
32crn 5670 . 2 class ran Singleton
41, 3wceq 1533 1 wff Singletons = ran Singleton
Colors of variables: wff setvar class
This definition is referenced by:  elsingles  35423
  Copyright terms: Public domain W3C validator