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

Definition df-succf 34844
Description: Define the successor function. See brsuccf 34913 for its value. (Contributed by Scott Fenton, 14-Apr-2014.)
Assertion
Ref Expression
df-succf Succ = (Cup ∘ ( I ⊗ Singleton))

Detailed syntax breakdown of Definition df-succf
StepHypRef Expression
1 csuccf 34820 . 2 class Succ
2 ccup 34818 . . 3 class Cup
3 cid 5574 . . . 4 class I
4 csingle 34810 . . . 4 class Singleton
53, 4ctxp 34802 . . 3 class ( I ⊗ Singleton)
62, 5ccom 5681 . 2 class (Cup ∘ ( I ⊗ Singleton))
71, 6wceq 1542 1 wff Succ = (Cup ∘ ( I ⊗ Singleton))
Colors of variables: wff setvar class
This definition is referenced by:  brsuccf  34913
  Copyright terms: Public domain W3C validator