Metamath Proof Explorer

Theorem nnesuc

Description: Exponentiation with a successor exponent. Definition 8.30 of TakeutiZaring p. 67. (Contributed by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion nnesuc 
|- ( ( A e. _om /\ B e. _om ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( A e. _om -> A e. On )
2 onesuc 
 |-  ( ( A e. On /\ B e. _om ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
3 1 2 sylan 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )