Definition df-1o 5384

Description: Define the ordinal number 1.

Assertion

Ref	Expression
df-1o	|- 1o = suc (/)

Detailed syntax breakdown of Definition df-1o

Step	Hyp	Ref	Expression
1		c1o 5379	. 2 class 1o
2		c0 3114	. . 3 class (/)
3	2	csuc 3845	. 2 class suc (/)
4	1, 3	wceq 1615	1 wff 1o = suc (/)

This definition is referenced by:  1on 5389  df1o2 5391  ordgt0ge1 5395  oa1suc 5415  om1 5427  oe1 5429  oelim2 5476  nnecl 5489  1onn 5511  0sdom1dom 5857  aleph1 6512  cfpwsdom 6528  nlt1pi 6628  indpi 6629  aleph1re 9350  bnj168 13431  sltval2 14909  axsltsolem1 14921  top2usne 15916

Copyright terms: Public domain