Metamath Proof Explorer

Theorem df2o2

Description: Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004)

Ref Expression
Assertion df2o2 
|- 2o = { (/) , { (/) } }

Proof

Step Hyp Ref Expression
1 df2o3 
 |-  2o = { (/) , 1o }
2 df1o2 
 |-  1o = { (/) }
3 2 preq2i 
 |-  { (/) , 1o } = { (/) , { (/) } }
4 1 3 eqtri 
 |-  2o = { (/) , { (/) } }