ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-9 Unicode version

Definition df-9 8423
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 8414 . 2  class  9
2 c8 8413 . . 3  class  8
3 c1 7295 . . 3  class  1
4 caddc 7297 . . 3  class  +
52, 3, 4co 5613 . 2  class  ( 8  +  1 )
61, 5wceq 1287 1  wff  9  =  ( 8  +  1 )
Colors of variables: wff set class
This definition is referenced by:  9re  8444  9pos  8461  8p1e9  8490  5p4e9  8498  6p3e9  8500  7p2e9  8501  9nn  8518  8lt9  8547  8p2e10  8888  9p9e18  8902  9t9e81  8937
  Copyright terms: Public domain W3C validator