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

Definition df-10 9991
Description: Define the number 10. See remarks under df-2 9983. (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 9982 . 2  class  10
2 c9 9981 . . 3  class  9
3 c1 8917 . . 3  class  1
4 caddc 8919 . . 3  class  +
52, 3, 4co 6013 . 2  class  ( 9  +  1 )
61, 5wceq 1649 1  wff  10  =  ( 9  +  1 )
Colors of variables: wff set class
This definition is referenced by:  10re  10005  10pos  10017  9p1e10  10035  5p5e10  10044  6p4e10  10047  7p3e10  10049  8p2e10  10050  10nn  10066  9lt10  10103  decsucc  10334  9p2e11  10369  0.999...  12578  3dvds  12832  bposlem4  20931  bposlem5  20932  rmydioph  26769
  Copyright terms: Public domain W3C validator