Metamath Proof Explorer


Theorem oe0m0

Description: Ordinal exponentiation with zero base and zero exponent. Proposition 8.31 of TakeutiZaring p. 67. (Contributed by NM, 31-Dec-2004)

Ref Expression
Assertion oe0m0 𝑜 = 1 𝑜

Proof

Step Hyp Ref Expression
1 0elon On
2 oe0m On 𝑜 = 1 𝑜
3 1 2 ax-mp 𝑜 = 1 𝑜
4 dif0 1 𝑜 = 1 𝑜
5 3 4 eqtri 𝑜 = 1 𝑜