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

Definition df-9 8754
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 8746 . 2  class  9
2 c8 8745 . . 3  class  8
3 c1 7589 . . 3  class  1
4 caddc 7591 . . 3  class  +
52, 3, 4co 5742 . 2  class  ( 8  +  1 )
61, 5wceq 1316 1  wff  9  =  ( 8  +  1 )
Colors of variables: wff set class
This definition is referenced by:  9re  8775  9pos  8792  9m1e8  8814  8p1e9  8828  5p4e9  8836  6p3e9  8838  7p2e9  8839  9nn  8856  8lt9  8885  8p2e10  9229  9p9e18  9243  9t9e81  9278
  Copyright terms: Public domain W3C validator