Metamath Proof Explorer

Theorem 0exp0e1

Description: The zeroth power of zero equals one. See comment of exp0 . (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion 0exp0e1 
|- ( 0 ^ 0 ) = 1

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 exp0 
 |-  ( 0 e. CC -> ( 0 ^ 0 ) = 1 )
3 1 2 ax-mp 
 |-  ( 0 ^ 0 ) = 1