Proof of Ordered Pairs in a Map between Classes: Membership as a Value, and the Components Lie in the Domain and the Codomain

By Functions, Values of a Function, and Functions from One Class to Another (iii), $F$ is a function with $\operatorname{dom}F=A$ and $\operatorname{ran}F\subseteq B$.

Proof of (i). Let $a\in A$ and let $b$ be a set. Since $a\in\operatorname{dom}F$, the value $F(a)$ is defined, and by Functions, Values of a Function, and Functions from One Class to Another (ii) it is the unique set $v$ with $(a,v)\in F$; in particular

$$(a,F(a))\in F.$$

If $F(a)=b$, this says $(a,b)\in F$. Conversely, if $(a,b)\in F$, then $(a,b)\in F$ and $(a,F(a))\in F$ give $b=F(a)$ by single-valuedness of $F$ (Functions, Values of a Function, and Functions from One Class to Another (i)).

Proof of (ii). Let $a$ and $b$ be sets with $(a,b)\in F$. Then $a\in A$ by Domains and Restrictions of Maps (i). Since $\exists u\,((u,b)\in F)$ holds with $u=a$, $b\in\operatorname{ran}F$ by Relations, Domain, Range, Inverse and Composition (iii) (membership in a class abstraction, Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i)). Since $\operatorname{ran}F\subseteq B$, $b\in B$ by Subclasses and Subsets (i).