Description: Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of Mendelson p. 255. (Contributed by NM, 17-Dec-2003) (Revised by Mario Carneiro, 15-Nov-2014) (Proof shortened by AV, 17-Jul-2022)
|- A e. _V
|- B e. _V
|- ( A ^m { B } ) ~~ A
|- ( A e. _V -> A e. _V )
|- ( A e. _V -> B e. _V )
|- ( A e. _V -> ( A ^m { B } ) ~~ A )