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

Definition df-10 10071
Description: Define the number 10. See remarks under df-2 10063. (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 10062 . 2  class  10
2 c9 10061 . . 3  class  9
3 c1 8996 . . 3  class  1
4 caddc 8998 . . 3  class  +
52, 3, 4co 6084 . 2  class  ( 9  +  1 )
61, 5wceq 1653 1  wff  10  =  ( 9  +  1 )
Colors of variables: wff set class
This definition is referenced by:  10re  10085  10pos  10097  9p1e10  10115  5p5e10  10124  6p4e10  10127  7p3e10  10129  8p2e10  10130  10nn  10146  9lt10  10183  decsucc  10414  9p2e11  10449  0.999...  12663  3dvds  12917  bposlem4  21076  bposlem5  21077  rmydioph  27098
  Copyright terms: Public domain W3C validator