df-4o - Intuitionistic Logic Explorer

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

Definition df-4o 6004

Description: Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.)

**Assertion**
Ref	Expression
df-4o	⊢ 4_𝑜 = suc 3_𝑜

**Detailed syntax breakdown of Definition df-4o**
Step	Hyp	Ref	Expression
1		c4o 5997	. 2 class 4_𝑜
2		c3o 5996	. . 3 class 3_𝑜
3	2	csuc 4102	. 2 class suc 3_𝑜
4	1, 3	wceq 1243	1 wff 4_𝑜 = suc 3_𝑜

Colors of variables: wff set class

This definition is referenced by: 4on 6012 4onn 6096