Definition df-6o 35858

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

Assertion

Ref	Expression
df-6o	⊢ 6o = suc 5o

Detailed syntax breakdown of Definition df-6o

Step	Hyp	Ref	Expression
1		c6o 35853	. 2 class 6o
2		c5o 35852	. . 3 class 5o
3	2	csuc 6379	. 2 class suc 5o
4	1, 3	wceq 1570	1 wff 6o = suc 5o

This definition is used by:  6on  35863  6onn  35868  5olt9o  35875  gdlopcfv6  35976  gdlopcfv7  35977  gdlopcfv8  35978