Maps from Functional Predicative Relations, and Families of Sections

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $u$ and $v$ be distinct set variables, and let $\psi(u,v)$ be a predicative formula whose free variables are among $u$, $v$ and further variables, its parameters, with fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i); for sets $u$ and $v$, $\psi(u,v)$ is read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv). Let $(u,v)$ be the ordered pair.

(i) The relation. There is a relation $R_{\psi}$ such that for all sets $u$ and $v$: $(u,v)\in R_{\psi}$ if and only if $\psi(u,v)$.

(ii) Maps. Let $A$ and $B$ be classes such that every $u\in A$ has some $v\in B$ with $\psi(u,v)$, and such that $v=v'$ whenever $u\in A$, $v,v'\in B$, $\psi(u,v)$ and $\psi(u,v')$. Then there is a map $f:A\to B$ with $\psi(u,f(u))$ for every $u\in A$.

(iii) Families of sections. Let $A$ and $R$ be classes and $b$ a set. There is a map $f:A\to\mathcal{P}(b)$ into the power set of $b$ whose value at each $u\in A$ has as elements exactly the $w\in b$ with $(u,w)\in R$:

$$w\in f(u)\quad\text{if and only if}\quad w\in b\ \text{and}\ (u,w)\in R\qquad(u\in A).$$