Domains and Restrictions of Maps

This lemma adopts the setting of Sets and Maps: Ordinary Notation. Here $A$, $B$ and $C$ are classes, which may be proper classes, as Sets and Maps: Ordinary Notation §letters allows: the maps below are those of Functions, Values of a Function, and Functions from One Class to Another §map between classes, not only the maps between sets of Sets and Maps: Ordinary Notation §maps. Let $F:A\to B$ be a map, with $(a,b)$ the ordered pair.

¶ For all sets $a$ and $b$: if $(a,b)\in F$, then $a\in A$.

¶ If $C\subseteq A$, where $\subseteq$ is the subclass relation, then the restriction $F|_{C}$ of $F$ to $C$ is a map $F|_{C}:C\to B$.

¶ If $C\subseteq A$, then every $c\in C$ lies in the domain $\operatorname{dom}(F|_{C})$, and $(F|_{C})(c)=F(c)$, with values as in Functions, Values of a Function, and Functions from One Class to Another §value.