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

Definition df-10 10026
Description: Define the number 10. See remarks under df-2 10018. (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 10017 . 2  class  10
2 c9 10016 . . 3  class  9
3 c1 8951 . . 3  class  1
4 caddc 8953 . . 3  class  +
52, 3, 4co 6044 . 2  class  ( 9  +  1 )
61, 5wceq 1649 1  wff  10  =  ( 9  +  1 )
Colors of variables: wff set class
This definition is referenced by:  10re  10040  10pos  10052  9p1e10  10070  5p5e10  10079  6p4e10  10082  7p3e10  10084  8p2e10  10085  10nn  10101  9lt10  10138  decsucc  10369  9p2e11  10404  0.999...  12617  3dvds  12871  bposlem4  21028  bposlem5  21029  rmydioph  26979
  Copyright terms: Public domain W3C validator