In Aczel’s book (draft) on constructive set theory (https://www1.maths.leeds.ac.uk/~rathjen/book.pdf) there is a proposition (4.2.4 on page 34) regarding when a class function exists. I’m not completely following the proof that is stated there. There are four main claims made in the proof. I’m going to walkthrough my understanding of each of them.
Claim 1: By assumption $\forall x \in A \exists ! y \phi(x,y)$. Let $\theta(x,z)$ be the formulae $\exists y [z = \langle x,y \rangle \land \phi(x,y)]$. Clearly, by assumption and the uniqueness of $y$ we conclude $\forall x \in A \exists ! z \theta(x,z)$.
Claim 2: The required class function is $F = \{z \ | \ \exists x \in A \theta(x,z) \}$.
Here we need to show three things. First, that as defined $F$ is a class function. Second, that $\text{dom}(F) = A$. Finally, that $\forall x \in A \phi(x,F(x))$. This is the main source of my confusion.
Claim 3: If G is any other class function satisfying the above then by the assumption of uniqueness we have $G(x) = F(x)$ and thus $G = F$.
Claim 4: If $A$ is a set then replacement guarantees the existence of a set $G$ such that $z \in G$ if and only if $\exists x \in A \theta(x,z)$ which holds if and only if $z \in F$. By extensionality, $F = G$ so it is a set.
I feel confident about my reasoning on Claims 1, 3 and 4, but please let me know if I have made any oversights.
In regards to Claim 2: does it matter what the range of $F$ is? To show it is a class function I (think that I) need to show that $F$ is a subset $A \times B$, but I don’t know what $B$ should be. I think satisfying the remaining properties of Claim 2 follows from the definition of $F$, but I don’t immediately see how. Any help would be appreciated. Thanks!
Edit: Our assumption $\forall x \in A \exists ! y \phi(x,y)$ can be specified to say $\forall x \in A \exists y \phi(x,y)$. This weakened statement is the hypothesis of strong collection (an axiom of CZF). From it we can infer the existence of a set $B$ such that $\forall x \in \exists y \in B \phi(x,y)$ and $\forall y \in B \exists x \in A \phi(x,y)$. This gets me a step closer to a set $B$ which could be the range of $F$ (again I am not sure if that is neccesary; see paragraph prior to edit), but from it (I think) we may NOT conlcude $\forall x \in A \exists ! y \in B \phi(x,y)$.
You should remind first that the notion of a class function is, in most cases, a synonym of a first-order definable class function. Moreover, we do not need to care about the exact range of a function when we define it. We already know the codomain of $F$: the class of all sets $V$.
You asked whether we need to show $F$ is a subset of $A\times B$ for some $B$. No, $F$ is a class function, and it means we do not want to care $F$ is a subset of $A\times B$. We already specified how to define $F$, and it demonstrates that $F$ is a definable class function. We should focus on that $A$ is a mere class, not a set.
Let me add some explanation for class functions to answer a question in a comment.
A class function is a class that satisfies functionality. That is, a class $F$ is class function is a class binary relation such that $(x,y),(x,z)\in F$ implies $y=z$.
First-order set theories, whether classical or constructive, do not have a notion of classes as themselves. Instead, classes over these theories are another way to describe set-theoretic formulas. In some sense, all classes over first-order set theories are definable, that is, they are of the form $\{x\in V \mid \phi(x,p)\}$ for some formula $\phi$ and a parameter $p$. You may understand class functions over first-order set theories like $\mathsf{ZF}$ or $\mathsf{CZF}$ under the frame mentioned just before: class function is another name for formulas $\phi(x,y)$ satisfying $\forall x\exists! y \phi(x,y)$.
The situation would be slightly different if we work over second-order set theories, like Gödel-Bernays set theory $\mathsf{GB}$. In that case, we do not need to rewrite classes to first-order formulas. Class functions are just class binary relations satisfying functionality, and there is nothing more.