Maps and Relations Given by Formulas

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation: this lemma is a scheme of the metatheory, asserting one lemma for each expression $t$ or formula $\varphi$ as below, possibly with parameters (sets or classes). In each clause, every defined set symbol occurring in $t$ or $\varphi$ is assumed to be used properly at the arguments indicated, and $\varphi$ quantifies over sets only.

¶ Let $a$ and $b$ be sets and $t(u)$ an expression with $t(u)\in b$ for every $u\in a$. Then there is exactly one map $f:a\to b$ with $f(u)=t(u)$ for every $u\in a$.

¶ Let $b$, $c$ and $d$ be sets and $t(v,w)$ an expression with $t(v,w)\in b$ for all $v\in c$ and $w\in d$. Then there is exactly one map $f:c\times d\to b$ with $f((v,w))=t(v,w)$ for all $v\in c$ and $w\in d$.

¶ Let $a$ be a set and $\varphi(u,v)$ a formula. Then there is exactly one relation $R$ on $a$ such that, for all $u,v\in a$, $(u,v)\in R$ if and only if $\varphi(u,v)$.