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

Definition df-10 9808
Description: Define the number 10. See remarks under df-2 9800. (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 9799 . 2  class  10
2 c9 9798 . . 3  class  9
3 c1 8734 . . 3  class  1
4 caddc 8736 . . 3  class  +
52, 3, 4co 5820 . 2  class  ( 9  +  1 )
61, 5wceq 1624 1  wff  10  =  ( 9  +  1 )
Colors of variables: wff set class
This definition is referenced by:  10re  9822  10pos  9834  9p1e10  9850  5p5e10  9859  6p4e10  9862  7p3e10  9864  8p2e10  9865  10nn  9881  9lt10  9918  decsucc  10147  9p2e11  10182  0.999...  12332  3dvds  12586  bposlem4  20521  bposlem5  20522  rmydioph  26507
  Copyright terms: Public domain W3C validator