Uhm, anything that is part of a definition follows from that definition.
`A and B implies A' and so on.
In the end a function, in the mathematical sense, is just a long (possibly infinite) table of `from' and `to' values. We could argue that one definition of ^ is more or less complex than another, for some definition of complexity, but I'm not sure which would win, and if it would be useful.
"Follows" in the sense that it is not an axiom - it has a proof of more than one line in the sense of the Hilbert system. Seeing functions as collections of ordered pairs tells us nothing here.
Your definition of ^ doesn't directly tell me that 2^1=2. It does tell me however that 0^0=1.
