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 7450

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 7443	. 2 class 4_𝑜
2		c3o 7442	. . 3 class 3_𝑜
3	2	csuc 5642	. 2 class suc 3_𝑜
4	1, 3	wceq 1475	1 wff 4_𝑜 = suc 3_𝑜

Colors of variables: wff setvar class

This definition is referenced by: 4on 7458 o2p2e4 7508 4onn 7609 en4 8083 hash4 13056