The Successor of a Set

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

¶ The successor of $x$ is the union $S(x)=x\cup\{x\}$ of $x$ and its singleton. It 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 §binary-union, and by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and The Empty Set, the Unordered Pair and the Singleton §singleton, for every set $u$,

$$u\in S(x)\quad\text{if and only if}\quad u\in x\ \text{or}\ u=x.$$

By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $S(x)$ is therefore the unique set $z$ satisfying the predicative formula $\forall u\,(u\in z\Leftrightarrow(u\in x\vee u=x))$, so $S(x)$ is a defined set symbol.