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_{𝑜}=\mathrm{suc}\varnothing$$

Detailed syntax breakdown

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