Proof of 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

We use twice that a class equal to a set is a set: if $A=z$ and $z\in W$ for a class $W$, then $A\in W$ by substitutivity of equality, which holds because $=$ is the equality of the underlying logic by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols, so $A$ is a set by Classes, Membership, Sets and Proper Classes §set.

Clause subclass. Let $A$ be a subclass of $x$. By Axiom of Separation for Classes applied to $x$ and $A$, there is a set $z$ such that, for every set $u$, $u\in z$ if and only if $u\in x$ and $u\in A$. By Subclasses and Subsets §subclass, every $u\in A$ satisfies $u\in x$, so for every set $u$, $u\in z$ if and only if $u\in A$. By Axiom of Extensionality for Classes, $A=z$, so $A$ is a set. For the particular cases, by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, for every set $u$ we have $u\in x\cap Y$ if and only if $u\in x$ and $u\in Y$, and $u\in x\setminus Y$ if and only if $u\in x$ and $u\notin Y$. Every element of $x\cap Y$ or of $x\setminus Y$ is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements, hence is an element of $x$. Thus $x\cap Y\subseteq x$ and $x\setminus Y\subseteq x$, and both are sets by what was just shown.

Clause union. By Axiom of Union there is a set $z$ such that, for every set $u$, $u\in z$ if and only if there is a set $v$ with $u\in v$ and $v\in x$. If $z'$ is a set with the same property, then for every set $u$, $u\in z$ if and only if $u\in z'$, both being equivalent to the same condition; so $z=z'$ by Axiom of Extensionality for Classes.

Clause power. By Axiom of Power Set there is a set $z$ such that, for every set $u$, $u\in z$ if and only if every set $w$ with $w\in u$ satisfies $w\in x$. For a set $u$, by Subclasses and Subsets §subclass, $u$ is a subset of $x$, written $u\subseteq x$, exactly when every element of $u$ is an element of $x$; since every element of $u$ is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements, this is equivalent to: every set $w$ with $w\in u$ satisfies $w\in x$. Hence for every set $u$, $u\in z$ if and only if $u$ is a subset of $x$. If $z'$ is a set with the same property, then for every set $u$, $u\in z$ if and only if $u$ is a subset of $x$, if and only if $u\in z'$, so $z=z'$ by Axiom of Extensionality for Classes.

Clause binary-union. By Axiom of Pairing there is a set $p$ such that, for every set $v$, $v\in p$ if and only if $v=x$ or $v=y$. By Axiom of Union applied to the set $p$, there is a set $z$ such that, for every set $u$, $u\in z$ if and only if there is a set $v$ with $u\in v$ and $v\in p$. For a set $u$, such a $v$ exists if and only if $u\in x$ or $u\in y$: if $u\in v$ and $v\in p$ then $v=x$ or $v=y$, so $u\in x$ or $u\in y$; conversely, if $u\in x$ take $v=x$, and if $u\in y$ take $v=y$, both sets lying in $p$. On the other hand, by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, for every set $u$, $u\in x\cup y$ if and only if $u\in x$ or $u\in y$. Hence $u\in x\cup y$ if and only if $u\in z$ for every set $u$, so $x\cup y=z$ by Axiom of Extensionality for Classes, and $x\cup y$ is a set.

Clause proper. The formula $u\notin u$, that is $\neg\,u\in u$, has no class quantifier, so it is predicative. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction the class $R=\{u:u\notin u\}$ exists, and for every set $u$, $u\in R$ if and only if $u\notin u$. Suppose, for a contradiction, that the universal class $V$ is a set. Every element of $R$ is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements, and every set is an element of $V$ by The Boolean Operations on Classes, Disjointness, and the Universal Class §universe; hence $R\subseteq V$ by Subclasses and Subsets §subclass. By clause subclass above applied to the set $V$, $R$ is a set. Taking $u=R$ in the defining property of $R$ gives $R\in R$ if and only if $R\notin R$, which is impossible. Hence $V$ is not a set, that is, $V$ is a proper class by Classes, Membership, Sets and Proper Classes §proper.