Metamath Proof Explorer


Definition df-9

Description: Define the number 9. (Contributed by NM, 27-May-1999)

Ref Expression
Assertion df-9
|- 9 = ( 8 + 1 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c9
 |-  9
1 c8
 |-  8
2 caddc
 |-  +
3 c1
 |-  1
4 1 3 2 co
 |-  ( 8 + 1 )
5 0 4 wceq
 |-  9 = ( 8 + 1 )