This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-3o

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

		Ref	Expression
	Assertion	df-3o	$⊢ 3_{𝑜} = suc 2_{𝑜}$

Step	Hyp	Ref	Expression
0		c3o	$class 3_{𝑜}$
1		c2o	$class 2_{𝑜}$
2	1	csuc	$class suc 2_{𝑜}$
3	0 2	wceq	$wff 3_{𝑜} = suc 2_{𝑜}$