Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-10 | GIF version |
Description: Define the number 10. See remarks under df-2 7973. (Contributed by NM, 5-Feb-2007.) |
Ref | Expression |
---|---|
df-10 | ⊢ 10 = (9 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c10 7972 | . 2 class 10 | |
2 | c9 7971 | . . 3 class 9 | |
3 | c1 6890 | . . 3 class 1 | |
4 | caddc 6892 | . . 3 class + | |
5 | 2, 3, 4 | co 5512 | . 2 class (9 + 1) |
6 | 1, 5 | wceq 1243 | 1 wff 10 = (9 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 10re 8004 10pos 8021 9p1e10 8051 5p5e10 8060 6p4e10 8063 7p3e10 8065 8p2e10 8066 10nn 8085 9lt10 8122 decsucc 8394 9p2e11 8429 |
Copyright terms: Public domain | W3C validator |