Definition df-1o 7132

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 7125	. 2 class 1o
2		c0 3770	. . 3 class (/)
3	2	csuc 4870	. 2 class suc (/)
4	1, 3	wceq 1383	1 wff 1o = suc (/)

This definition is referenced by:  1on  7139  df1o2  7144  ordgt0ge1  7149  oa1suc  7183  om1  7193  oe1  7195  oelim2  7246  nnecl  7264  1onn  7290  omabs  7298  nnm1  7299  0sdom1dom  7719  ackbij1lem14  8616  aleph1  8949  cfpwsdom  8962  nlt1pi  9287  indpi  9288  hash1  12448  aleph1re  13855  sltval2  29391  sltsolem1  29403  rankeq1o  29803  bnj168  33518  bj-1ex  34255