The Class of All Functions from One Set to Another

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $x$ and $y$ be sets.

¶ The class of functions from $x$ to $y$ is

$$y^{x}=\{f:f\text{ is a function from }x\text{ to }y\},$$

formed by class abstraction with parameters $x$ and $y$, where "$f$ is a function from $x$ to $y$" means $f:x\to y$ in the sense of Functions, Values of a Function, and Functions from One Class to Another §map. This condition is a predicative formula, since being a relation, being single-valued, having domain $x$ and having range included in $y$ are each expressed with quantifiers over sets only.