 Epsilon-recursion theorem

Given a definable operation $G(x,h)$ on a set $x$ and a function $h$ with domain $x$, there is a unique class function $F$ satisfyingfor every set $x$. Existence and uniqueness follow by epsilon induction, because the value at $x$ depends only on values at members of $x$.