MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-10 Structured version   Unicode version

Definition df-10 10066
Description: Define the number 10. See remarks under df-2 10058. (Contributed by NM, 5-Feb-2007.)
Assertion
Ref Expression
df-10  |-  10  =  ( 9  +  1 )

Detailed syntax breakdown of Definition df-10
StepHypRef Expression
1 c10 10057 . 2  class  10
2 c9 10056 . . 3  class  9
3 c1 8991 . . 3  class  1
4 caddc 8993 . . 3  class  +
52, 3, 4co 6081 . 2  class  ( 9  +  1 )
61, 5wceq 1652 1  wff  10  =  ( 9  +  1 )
Colors of variables: wff set class
This definition is referenced by:  10re  10080  10pos  10092  9p1e10  10110  5p5e10  10119  6p4e10  10122  7p3e10  10124  8p2e10  10125  10nn  10141  9lt10  10178  decsucc  10409  9p2e11  10444  0.999...  12658  3dvds  12912  bposlem4  21071  bposlem5  21072  rmydioph  27085
  Copyright terms: Public domain W3C validator