"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.
`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.