Functions, Values of a Function, and Functions from One Class to Another

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $F$, $A$ and $B$ be classes, and let $(u,v)$ denote the ordered pair.

¶ $F$ is a function if $F$ is a relation and, for all sets $u$, $v$ and $v'$, if $(u,v)\in F$ and $(u,v')\in F$ then $v=v'$.

¶ Let $F$ be a function and let $u$ be a set in the domain $\operatorname{dom}F$. The value of $F$ at $u$, written $F(u)$, is the unique set $v$ with $(u,v)\in F$: such a set exists because $u\in\operatorname{dom}F$, by Relations, Domain, Range, Inverse and Composition §domain and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, and it is unique by the defining property of a function above. Thus, for $u\in\operatorname{dom}F$, $F(u)$ is the unique set $z$ satisfying the predicative formula $(u,z)\in F$, in which $F$ is a class parameter, and it is used as a defined set symbol.

¶ $F$ is a function from $A$ to $B$, also called a map from $A$ to $B$ and written $F:A\to B$, if $F$ is a function, $\operatorname{dom}F=A$, and the range satisfies $\operatorname{ran}F\subseteq B$, where $\subseteq$ is the subclass relation.