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

Metamath Proof Explorer

Definition df-1o

Description: Define the ordinal number 1. Definition 2.1 of Schloeder p. 4. (Contributed by NM, 29-Oct-1995)

		Ref	Expression
	Assertion	df-1o	$⊢ 1_{𝑜} = suc \emptyset$

Step	Hyp	Ref	Expression
0		c1o	$class 1_{𝑜}$
1		c0	$class \emptyset$
2	1	csuc	$class suc \emptyset$
3	0 2	wceq	$wff 1_{𝑜} = suc \emptyset$