= Solution
A bounded expression for the successor relation is
$$
\boxed{y\in x\ \land\ (\forall z\in y\ z\in x)\ \land\ (\forall z\in x\ (z\in y\lor z=y)).}
$$
The first two clauses put $y$ and all its elements into $x$, while the last forbids any additional member of $x$. <Extensionality> identifies this exactly with $x=y\cup\{y\}$. Since the formula is $\Delta_0$, it is absolute in both directions between the transitive classes and therefore upward absolute. This bounded description also justifies the successor computations used earlier in the rank-stage <Replacement> counterexample.
Back to article page
