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

Definition df-10 9828
Description: Define the number 10. See remarks under df-2 9820. (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 9819 . 2  class  10
2 c9 9818 . . 3  class  9
3 c1 8754 . . 3  class  1
4 caddc 8756 . . 3  class  +
52, 3, 4co 5874 . 2  class  ( 9  +  1 )
61, 5wceq 1632 1  wff  10  =  ( 9  +  1 )
Colors of variables: wff set class
This definition is referenced by:  10re  9842  10pos  9854  9p1e10  9870  5p5e10  9879  6p4e10  9882  7p3e10  9884  8p2e10  9885  10nn  9901  9lt10  9938  decsucc  10167  9p2e11  10202  0.999...  12353  3dvds  12607  bposlem4  20542  bposlem5  20543  rmydioph  27210
  Copyright terms: Public domain W3C validator