Definition df-9o 35861

Description: Define the ordinal number 9. (Contributed by BTernaryTau, 2-Sep-2026.)

Assertion

Ref	Expression
df-9o	⊢ 9o = suc 8o

Detailed syntax breakdown of Definition df-9o

Step	Hyp	Ref	Expression
1		c9o 35856	. 2 class 9o
2		c8o 35855	. . 3 class 8o
3	2	csuc 6379	. 2 class suc 8o
4	1, 3	wceq 1570	1 wff 9o = suc 8o

This definition is used by:  9on  35866  9onn  35871  8olt9o  35872  jf1  36009  jf1o  36010  k39o  36016  jltalephlem  36024