Proof of Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set

Throughout, every element of a class is a set by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §objects, and $(a,b)$ is the ordered pair, 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.

Image-set. Let $x$ be a set. By Functions, Values of a Function, and Functions from One Class to Another §function, for all sets $v,u,u'$, if $(v,u)\in F$ and $(v,u')\in F$ then $u=u'$; this is exactly the hypothesis of the replacement axiom Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §replacement, applied to the class $F$. It yields a set $y$ such that, for every set $u$, $u\in y$ if and only if there is a set $v$ with $v\in x$ and $(v,u)\in F$. By The Image and the Preimage of a Class under a Class §image, the same condition characterizes $u\in F[x]$. Hence $F[x]=y$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, and $F[x]$ is a set.

Function-set. Let $x=\operatorname{dom}F$ be a set. By the clause image-set above, $F[x]$ is a set, so the Cartesian product $x\times F[x]$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set. 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,v$; then $u\in\operatorname{dom}F=x$ by Relations, Domain, Range, Inverse and Composition §domain, and $v\in F[x]$ by The Image and the Preimage of a Class under a Class §image, since $u\in x$ and $(u,v)\in F$. So $p\in x\times F[x]$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. Hence $F\subseteq x\times F[x]$ by Subclasses and Subsets §subclass, and $F$ 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.