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 8810

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 8802	. 2 class 9
2		c8 8801	. . 3 class 8
3		c1 7645	. . 3 class 1
4		caddc 7647	. . 3 class +
5	2, 3, 4	co 5782	. 2 class (8 + 1)
6	1, 5	wceq 1332	1 wff 9 = (8 + 1)

Colors of variables: wff set class

This definition is referenced by: 9re 8831 9pos 8848 9m1e8 8870 8p1e9 8884 5p4e9 8892 6p3e9 8894 7p2e9 8895 9nn 8912 8lt9 8941 8p2e10 9285 9p9e18 9299 9t9e81 9334