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

Definition df-succf 25716
Description: Define the successor function. See brsuccf 25786 for its value. (Contributed by Scott Fenton, 14-Apr-2014.)
Assertion
Ref Expression
df-succf  |- Succ  =  (Cup 
o.  (  _I  (x) Singleton ) )

Detailed syntax breakdown of Definition df-succf
StepHypRef Expression
1 csuccf 25692 . 2  class Succ
2 ccup 25690 . . 3  class Cup
3 cid 4493 . . . 4  class  _I
4 csingle 25682 . . . 4  class Singleton
53, 4ctxp 25674 . . 3  class  (  _I 
(x) Singleton )
62, 5ccom 4882 . 2  class  (Cup  o.  (  _I  (x) Singleton ) )
71, 6wceq 1652 1  wff Succ  =  (Cup 
o.  (  _I  (x) Singleton ) )
Colors of variables: wff set class
This definition is referenced by:  brsuccf  25786
  Copyright terms: Public domain W3C validator