Axiom Schema of Specification - in NBG Class Theory

In NBG Class Theory

In von Neumann–Bernays–Gödel set theory, a distinction is made between sets and classes. A class C is a set if and only if it belongs to some class E. In this theory, there is a theorem schema that reads:

that is:

There is a class D such that any class C is a member of D if and only if C is a set that satisfies P.

This theorem schema is itself a restricted form of comprehension, which avoids Russell's paradox because of the requirement that C be a set. Then specification for sets themselves can be written as a single axiom:

that is:

Given any class D and any set A, there is a set B whose members are precisely those classes that are members of both A and D;

or even more simply:

The intersection of a class D and a set A is itself a set B.

In this axiom, the predicate P is replaced by the class D, which can be quantified over.