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 6027

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 6020	. 2 class 4_𝑜
2		c3o 6019	. . 3 class 3_𝑜
3	2	csuc 4120	. 2 class suc 3_𝑜
4	1, 3	wceq 1284	1 wff 4_𝑜 = suc 3_𝑜

Colors of variables: wff set class

This definition is referenced by: 4on 6035 4onn 6119