Powers with a Variable Base: a Predicative Formula and the Map (x, m) ↦ $x^m$

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, with predicative meant for formulas with abbreviations, conditions expressed by a predicative formula are as in Conditions Expressed by a Predicative Formula, and Guards (ii), with parameters and their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). Let $\cdot$ be a binary operation on a set $X$ with a neutral element $e$, the only one by A Binary Operation Has at Most One Neutral Element (i); for $x\in X$ and $m\in\mathbb{N}_{0}$, $x^{m}$ is the power of Powers with Exponents in the Natural Numbers with Zero (i) and Powers with Exponents in the Natural Numbers with Zero (ii), so that $x^{0}=e$.

(i) This clause is a statement of the metatheory. The letters $x$, $m$ and $z$ are distinct set variables, and $X$, $\cdot$, $e$, $\mathbb{N}$, $\mathbb{N}_{0}$, and the order $\le$, the addition $+$ and the element $0$ of $\mathbb{N}_{0}$ are parameters. Then the condition "$x\in X$, $m\in\mathbb{N}_{0}$ and $z=x^{m}$" on $x$, $m$ and $z$ is expressed by a predicative formula.

(ii) There is exactly one map $p:X\times\mathbb{N}_{0}\to X$, with $X\times\mathbb{N}_{0}$ the Cartesian product, with $p(x,m)=x^{m}$ for all $x\in X$ and $m\in\mathbb{N}_{0}$.