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

Definition df-10 9812
Description: Define the number 10. See remarks under df-2 9804. (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 9803 . 2  class  10
2 c9 9802 . . 3  class  9
3 c1 8738 . . 3  class  1
4 caddc 8740 . . 3  class  +
52, 3, 4co 5858 . 2  class  ( 9  +  1 )
61, 5wceq 1623 1  wff  10  =  ( 9  +  1 )
Colors of variables: wff set class
This definition is referenced by:  10re  9826  10pos  9838  9p1e10  9854  5p5e10  9863  6p4e10  9866  7p3e10  9868  8p2e10  9869  10nn  9885  9lt10  9922  decsucc  10151  9p2e11  10186  0.999...  12337  3dvds  12591  bposlem4  20526  bposlem5  20527  rmydioph  27107
  Copyright terms: Public domain W3C validator