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

Definition df-10 7979
Description: Define the number 10. See remarks under df-2 7971. (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 7970 . 2 class 10
2 c9 7969 . . 3 class 9
3 c1 6888 . . 3 class 1
4 caddc 6890 . . 3 class +
52, 3, 4co 5512 . 2 class (9 + 1)
61, 5wceq 1243 1 wff 10 = (9 + 1)
Colors of variables: wff set class
This definition is referenced by:  10re  8002  10pos  8019  9p1e10  8049  5p5e10  8058  6p4e10  8061  7p3e10  8063  8p2e10  8064  10nn  8083  9lt10  8120  decsucc  8392  9p2e11  8427
  Copyright terms: Public domain W3C validator