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

Definition df-10 10058
Description: Define the number 10. See remarks under df-2 10050. (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 10049 . 2  class  10
2 c9 10048 . . 3  class  9
3 c1 8983 . . 3  class  1
4 caddc 8985 . . 3  class  +
52, 3, 4co 6073 . 2  class  ( 9  +  1 )
61, 5wceq 1652 1  wff  10  =  ( 9  +  1 )
Colors of variables: wff set class
This definition is referenced by:  10re  10072  10pos  10084  9p1e10  10102  5p5e10  10111  6p4e10  10114  7p3e10  10116  8p2e10  10117  10nn  10133  9lt10  10170  decsucc  10401  9p2e11  10436  0.999...  12650  3dvds  12904  bposlem4  21063  bposlem5  21064  rmydioph  27066
  Copyright terms: Public domain W3C validator