well-founded recursion

Theorem 1.

Let $G$ be a binary (class) function on $V$, the class of all sets. Let $A$ be a well-founded set (with $R$ the well-founded relation). Then there is a unique function $F$ such that

$$F(x)=G(x,F|\mathrm{seg}(x)),$$

where $\mathrm{seg}\mathit{}\mathrm{(}x\mathrm{)}\mathrm{:=}\mathrm{\{}y\mathrm{\in }A\mathrm{\mid }y\mathit{}R\mathit{}x\mathrm{\}}$, the initial segment of $x$.

Remark. Since every well-ordered set is well-founded, the well-founded recursion theorem is a generalization of the transfinite recursion theorem. Notice that the $G$ here is a function in two arguments, and that it is necessary to specify the element $x$ in the first argument (in contrast with the $G$ in the transfinite recursion theorem), since it is possible that $\mathrm{seg}(a)=\mathrm{seg}(b)$ for $a\ne b$ in a well-founded set.

By converting $G$ into a formula ($\phi (x,y,z)$ such that for all $x,y$, there is a unique $z$ such that $\phi (x,y,z)$), then the above theorem can be proved in ZF (with the aid of the well-founded induction). The proof is similar to the proof of the transfinite recursion theorem.