df-9 - Intuitionistic Logic Explorer

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

Definition df-9 8981

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**
Step	Hyp	Ref	Expression
1		c9 8973	. 2 class 9
2		c8 8972	. . 3 class 8
3		c1 7809	. . 3 class 1
4		caddc 7811	. . 3 class +
5	2, 3, 4	co 5872	. 2 class (8 + 1)
6	1, 5	wceq 1353	1 wff 9 = (8 + 1)

Colors of variables: wff set class

This definition is referenced by: 9re 9002 9pos 9019 9m1e8 9041 8p1e9 9055 5p4e9 9063 6p3e9 9065 7p2e9 9066 9nn 9083 8lt9 9112 8p2e10 9459 9p9e18 9473 9t9e81 9508 lgsdir2lem5 14304