The Restriction of a Function or Relation to a Class

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $F$ and $A$ be classes.

¶ The restriction of $F$ to $A$ is the class

$$F|_{A}=\{p\in F:\exists u\,\exists v\,(p=(u,v)\wedge u\in A)\},$$

formed by restricted class abstraction. Here $(u,v)$ is the ordered pair, used as a defined set symbol, and the formula quantifies over set variables only, so it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires.