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

Each result cited is universally quantified over the data in its own statement.

By Functions, Values of a Function, and Functions from One Class to Another §map, $f$ is a function with domain $\operatorname{dom}f=A$ and range $\operatorname{ran}f\subseteq B$.

Clause value. Let $a\in A$ and let $b$ be a set. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, applied to the function $f$ and the sets $a$ and $b$, the statement "$a\in\operatorname{dom}f$ and $b=f(a)$" holds if and only if $(a,b)\in f$. Since $a\in A=\operatorname{dom}f$, the first part of that statement holds, so $(a,b)\in f$ if and only if $f(a)=b$.

Clause graph. Let $a\in A$. By Functions, Values of a Function, and Functions from One Class to Another §value, $f(a)$ is a set, so the clause value with $b=f(a)$ gives $(a,f(a))\in f$. Hence $f(a)\in\operatorname{ran}f$ by Relations, Domain, Range, Inverse and Composition §range and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, and since $\operatorname{ran}f\subseteq B$, $f(a)\in B$ by Subclasses and Subsets §subclass.

Clause restriction. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, $f|_{A}$ is a function with domain $A\cap\operatorname{dom}f=A\cap A$ and $(f|_{A})(u)=f(u)$ for every set $u\in A\cap A$. For every set $w$, $w\in A\cap A$ if and only if $w\in A$ and $w\in A$, by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, that is, if and only if $w\in A$; so $A\cap A=A$ by Axiom of Extensionality for Classes. Thus $f|_{A}$ and $f$ are functions with the same domain $A$ and with $(f|_{A})(u)=f(u)$ for every $u\in A$, and $f|_{A}=f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality.

Clause equality. By Functions, Values of a Function, and Functions from One Class to Another §map, $g$ is a function with $\operatorname{dom}g=A=\operatorname{dom}f$, and $g(a)=f(a)$ for every $a\in\operatorname{dom}g$ by hypothesis. Hence $g=f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality.

Clause map-symbol. Predicativity. The formula $\mu(h,A,B)$ is the formula $\mu(F,A,B)$ 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 with $h$ put for $F$; as displayed there it is written with the ordered pair as a defined set symbol and quantifies over set variables only, the variable $h$ being a set variable and its bound variables being renamed where necessary as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols. The part $\forall u\,(u\in A\Rightarrow(u,t(u,v_{1},\dots,v_{k}))\in h)$ is written with the ordered pair and the defined set symbols of $t$, quantifies over the set variable $u$ only, and no class abstraction is written in it, since none is written in $t$. So $\theta$ is an expression written with abbreviations in which no quantifier is applied to a class variable, and it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure.

Uniqueness. Fix sets $v_{1},\dots,v_{k}$ satisfying $\gamma$. By hypothesis, $t(u,v_{1},\dots,v_{k})$ is used properly and lies in $B$ for every $u\in A$; so Maps and Relations Given by Formulas §map, applied to the sets $A$ and $B$ and the expression $t(u,v_{1},\dots,v_{k})$ with $v_{1},\dots,v_{k}$ and the further free variables of $t$ as parameters, gives exactly one map $f_{v}:A\to B$ with $f_{v}(u)=t(u,v_{1},\dots,v_{k})$ for every $u\in A$; this is the map $u\mapsto t(u,v_{1},\dots,v_{k})$ of Sets and Maps: Ordinary Notation §maps, and it is a set by Sets and Maps: Ordinary Notation §maps.

Let $h$ be a set. By 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 (by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §renaming if $A$ and $B$ are the same variable), $\mu(h,A,B)$ holds if and only if $h$ is a map $h:A\to B$. For $u\in A$, the defined set symbols of $t$ are used properly in the part $(u,t(u,v_{1},\dots,v_{k}))\in h$, so by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination, applied to each of them in turn, and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §pair-membership, this part holds if and only if the ordered pair of $u$ and the set $t(u,v_{1},\dots,v_{k})$ is an element of $h$. When $h:A\to B$ is a map, this holds for every $u\in A$ if and only if $h(u)=t(u,v_{1},\dots,v_{k})$ for every $u\in A$, by the clause value applied to the map $h$ and the set $b=t(u,v_{1},\dots,v_{k})$. Hence $\theta(h,v_{1},\dots,v_{k})$ holds if and only if $h$ is a map $h:A\to B$ with $h(u)=t(u,v_{1},\dots,v_{k})$ for every $u\in A$, that is, by the uniqueness above, if and only if $h=f_{v}$. So $f_{v}$ is the only set satisfying $\theta(h,v_{1},\dots,v_{k})$.