Metamath Proof Explorer

Theorem df1o2

Description: Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002)

Ref Expression
Assertion df1o2 
|- 1o = { (/) }

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 suc0 
 |-  suc (/) = { (/) }
3 1 2 eqtri 
 |-  1o = { (/) }