Inductive Classes

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $A$ be a class, and let $S(u)$ denote the successor of a set $u$.

¶ $A$ is inductive if the empty set satisfies $\emptyset\in A$ and $S(u)\in A$ for every $u\in A$. This is the defined predicate abbreviating $\emptyset\in A\wedge\forall u\,(u\in A\Rightarrow S(u)\in A)$, with $u$ a set variable; $\emptyset$ and $S(u)$ are defined set symbols, so the formula is predicative.