# Definition by recursion of class valued functions

Let $\tau(\alpha,X)$ be a class term and let G be a function on $On\times V$ such that for all $\alpha$ and y, $G(\alpha,y)\subseteq\alpha\times V$. We also assume that for every $X\subseteq\alpha\times V$ we can prove that $y\in\tau(\alpha,X)\leftrightarrow y\in\tau(\alpha,X\cap G(\alpha,y))$. Then there is a unique class $A\subseteq On\times V$ such that for all $\alpha$, $A_{\alpha}=\tau(\alpha,A\upharpoonright\alpha)$, where $A_{\alpha}=\{z \ |\ \langle\alpha,z\rangle\in A\}=A[\{\alpha\}]$.

(This question is an exercise of Levy's book "Basic Set Theory"(Chapter IV, 4.27 Exercise).)

-
Posted on MO: mathoverflow.net/questions/104703 –  Asaf Karagila Aug 14 '12 at 16:22
Closed on MO. $\:$ –  Ricky Demer Aug 14 '12 at 19:51
How to prove this theorem? (the method in the proof of definition by recursion of set valued functions can't be extended to this one) –  Sencodian Aug 15 '12 at 5:31
And how to use the condition "y∈τ(α,X)↔y∈τ(α,X∩G(α,y))" ? –  Sencodian Aug 15 '12 at 5:33