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

Definition df-10 10022
Description: Define the number 10. See remarks under df-2 10014. (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 10013 . 2  class  10
2 c9 10012 . . 3  class  9
3 c1 8947 . . 3  class  1
4 caddc 8949 . . 3  class  +
52, 3, 4co 6040 . 2  class  ( 9  +  1 )
61, 5wceq 1649 1  wff  10  =  ( 9  +  1 )
Colors of variables: wff set class
This definition is referenced by:  10re  10036  10pos  10048  9p1e10  10066  5p5e10  10075  6p4e10  10078  7p3e10  10080  8p2e10  10081  10nn  10097  9lt10  10134  decsucc  10365  9p2e11  10400  0.999...  12613  3dvds  12867  bposlem4  21024  bposlem5  21025  rmydioph  26975
  Copyright terms: Public domain W3C validator