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

Definition df-9 10021
Description: Define the number 9. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-9  |-  9  =  ( 8  +  1 )

Detailed syntax breakdown of Definition df-9
StepHypRef Expression
1 c9 10012 . 2  class  9
2 c8 10011 . . 3  class  8
3 c1 8947 . . 3  class  1
4 caddc 8949 . . 3  class  +
52, 3, 4co 6040 . 2  class  ( 8  +  1 )
61, 5wceq 1649 1  wff  9  =  ( 8  +  1 )
Colors of variables: wff set class
This definition is referenced by:  9re  10035  9pos  10047  8p1e9  10065  5p4e9  10074  6p3e9  10077  7p2e9  10079  8p2e10  10081  9nn  10096  8lt9  10126  9p9e18  10407  9t9e81  10440  19prm  13395  139prm  13401  log2tlbnd  20738  bposlem8  21028  lgsdir2lem5  21064  rmydioph  26975
  Copyright terms: Public domain W3C validator