Proof of The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set

Membership in a class formed by class abstraction is unfolded by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction; class abstractions are unfolded without further mention.

Members. Let $F$ be a class. If $F\in y^{x}$, then $F$ is a set by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §objects, and $F:x\to y$ by The Class of All Functions from One Set to Another §functions. Conversely, let $F:x\to y$. Then $F$ is a function whose domain $\operatorname{dom}F=x$ is a set, by Functions, Values of a Function, and Functions from One Class to Another §map, so $F$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set; hence $F\in y^{x}$ by The Class of All Functions from One Set to Another §functions.

Set. By Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set the Cartesian product $x\times y$ is a set, so its power set $\mathcal{P}(x\times y)$ exists by The Union Set and the Power Set of a Set §power.

Let $f\in y^{x}$. By the clause members above, $f:x\to y$; that is, by Functions, Values of a Function, and Functions from One Class to Another §map, $f$ is a function, $\operatorname{dom}f=x$ and $\operatorname{ran}f\subseteq y$. Let $p\in f$. Since $f$ is a relation by Functions, Values of a Function, and Functions from One Class to Another §function, $p=(u,v)$ for some sets $u$ and $v$. Then $u\in\operatorname{dom}f=x$ by Relations, Domain, Range, Inverse and Composition §domain, and $v\in\operatorname{ran}f$ by Relations, Domain, Range, Inverse and Composition §range, so $v\in y$ by Subclasses and Subsets §subclass. By Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, $p=(u,v)\in x\times y$. Hence $f\subseteq x\times y$, so $f\in\mathcal{P}(x\times y)$ by The Union Set and the Power Set of a Set §power.

As $f$ was arbitrary, $y^{x}\subseteq\mathcal{P}(x\times y)$ by Subclasses and Subsets §subclass, and $y^{x}$ is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass.