 Axiom of set comprehension: For any formula \(\phi (x)\) which does not mention the sethood predicate and in which all free variables other than \(x\) denote sets, and which further has the property that \(\phi(x)\) is only true of sets \(x\), the class \(\{x \mid \phi \}\) (which exists by Class Comprehension since all suitable \(x\) are sets) is a set.