Metamath Proof Explorer


Theorem 0exp0e1

Description: 0 ^ 0 = 1 . This is our convention. It follows the convention used by Gleason; see Part of Definition 10-4.1 of Gleason p. 134. (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion 0exp0e1 0 0 = 1

Proof

Step Hyp Ref Expression
1 0cn 0
2 exp0 0 0 0 = 1
3 1 2 ax-mp 0 0 = 1