Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol

This helper adopts the setting of Sets and Maps: Ordinary Notation. In the clauses value, graph, restriction and equality, $A$ and $B$ are sets and $f:A\to B$ is a map, with values $f(a)$ for $a\in A$.

¶ For every $a\in A$ and every set $b$: $(a,b)\in f$ if and only if $f(a)=b$.

¶ For every $a\in A$: $(a,f(a))\in f$ and $f(a)\in B$.

¶ The restriction of $f$ to $A$ is $f$: $f|_{A}=f$.

¶ If $g:A\to B$ is a map with $g(a)=f(a)$ for every $a\in A$, then $g=f$.

¶ Let $A$ and $B$ be sets, let $k\ge0$ be a metatheoretic number, let $v_{1},\dots,v_{k}$, $u$ and $h$ be distinct set variables, distinct from $A$ and $B$, and let $\gamma(v_{1},\dots,v_{k})$ be a predicative formula, predicative being meant, here and below, for formulas with abbreviations; and let $t(u,v_{1},\dots,v_{k})$ be an expression built from variables and defined set symbols, with no class abstraction written in it, such that for all sets $v_{1},\dots,v_{k}$ satisfying $\gamma$ and every $u\in A$, $t(u,v_{1},\dots,v_{k})$ is used properly and lies in $B$; $A$, $B$ and the further free variables of $\gamma$ and $t$ are parameters, $h$ occurring in neither. Let $\theta(h,v_{1},\dots,v_{k})$ be the formula $\mu(h,A,B)\wedge\forall u\,(u\in A\Rightarrow(u,t(u,v_{1},\dots,v_{k}))\in h)$, with $\mu$ the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §map. Then $\theta$ is predicative, and for all sets $v_{1},\dots,v_{k}$ satisfying $\gamma$, the only set $h$ satisfying $\theta(h,v_{1},\dots,v_{k})$ is the map $u\mapsto t(u,v_{1},\dots,v_{k})$ from $A$ to $B$ of Sets and Maps: Ordinary Notation §maps.