Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
df1o2
Next ⟩
df2o3
Metamath Proof Explorer
Ascii
Structured
Theorem
df1o2
Description:
Expanded value of the ordinal number 1.
(Contributed by
NM
, 4-Nov-2002)
Ref
Expression
Assertion
df1o2
⊢
1
_{o}
= { ∅ }
Proof
Step
Hyp
Ref
Expression
1
df-1o
⊢
1
_{o}
= suc ∅
2
suc0
⊢
suc ∅ = { ∅ }
3
1
2
eqtri
⊢
1
_{o}
= { ∅ }