df-4o - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-4o		Structured version Visualization version GIF version

Definition df-4o 7563

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 7556	. 2 class 4_𝑜
2		c3o 7555	. . 3 class 3_𝑜
3	2	csuc 5725	. 2 class suc 3_𝑜
4	1, 3	wceq 1483	1 wff 4_𝑜 = suc 3_𝑜

Colors of variables: wff setvar class

This definition is referenced by: 4on 7571 o2p2e4 7621 4onn 7722 en4 8198 hash4 13195