Definition df-1o 6687

Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
df-1o	⊢ 1o = suc ∅

Detailed syntax breakdown of Definition df-1o

Step	Hyp	Ref	Expression
1		c1o 6680	. 2 class 1o
2		c0 3520	. . 3 class ∅
3	2	csuc 4510	. 2 class suc ∅
4	1, 3	wceq 1402	1 wff 1o = suc ∅

This definition is used by:  1on  6694  df1o2  6701  ordgt0ge1  6708  oa1suc  6740  1onn  6793  nnm1  6798  nlt1pig  7709  indpi  7710  1tonninf  10893  hash1  11268  012of  17194  2o01f  17195  pwle2  17199  isomninnlem  17250  iswomninnlem  17271  ismkvnnlem  17274