Proof of Domains and Restrictions of Maps

Throughout, every element of a class is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements; membership in a class formed by abstraction (the domain and range below) is read off by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted; and $X\subseteq Y$ is unfolded as "every element of $X$ is an element of $Y$" by Subclasses and Subsets §subclass. These three references cover those steps wherever they occur below.

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 domain. Let $a$ and $b$ be sets with $(a,b)\in F$. Then $a$ satisfies $\exists v\,((a,v)\in F)$, with witness $v=b$, so $a\in\operatorname{dom}F=A$ by Relations, Domain, Range, Inverse and Composition §domain.

Clause restriction-map. Assume $C\subseteq A$. Applying Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction with the class $C$ in the role of its $A$, $F|_{C}$ is a function with domain $\operatorname{dom}(F|_{C})=C\cap\operatorname{dom}F=C\cap A$. This intersection is $C$: by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations a set lies in $C\cap A$ if and only if it lies in $C$ and in $A$, and since $C\subseteq A$ every set in $C$ lies in $A$, so a set lies in $C\cap A$ if and only if it lies in $C$; hence $C\cap A=C$ by Axiom of Extensionality for Classes, and $\operatorname{dom}(F|_{C})=C$. For the range, let $v\in\operatorname{ran}(F|_{C})$. By Relations, Domain, Range, Inverse and Composition §range there is a set $u$ with $(u,v)\in F|_{C}$; every element of $F|_{C}$ is an element of $F$ by The Restriction of a Function or Relation to a Class §restriction, so $(u,v)\in F$. Then $v\in\operatorname{ran}F$, again by Relations, Domain, Range, Inverse and Composition §range, and $v\in B$ since $\operatorname{ran}F\subseteq B$. Hence $\operatorname{ran}(F|_{C})\subseteq B$. Thus $F|_{C}$ is a function with $\operatorname{dom}(F|_{C})=C$ and $\operatorname{ran}(F|_{C})\subseteq B$, that is, a map $F|_{C}:C\to B$ by Functions, Values of a Function, and Functions from One Class to Another §map.

Clause restriction-value. Assume $C\subseteq A$ and let $c\in C$. By the clause restriction-map, $F|_{C}$ is a function with $\operatorname{dom}(F|_{C})=C$, so $c\in\operatorname{dom}(F|_{C})$, which is the first assertion. Also $c\in A=\operatorname{dom}F$, so both values $F(c)$ and $(F|_{C})(c)$ are defined by Functions, Values of a Function, and Functions from One Class to Another §value, and $c\in C\cap\operatorname{dom}F$ by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations. Applying Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction with $C$ in the role of its $A$ and $c$ in the role of its $u$ gives $(F|_{C})(c)=F(c)$.