In this section, we give a sketch of the proof of the Eliminability Theorem for class terms in an extensional set theory where quantification occurs only over set variables.
Eliminability of class variables using the $a-statements ax-ext, df-clab, df-cleq, df-clel is an easy result, proved for instance in Appendix X of Azriel Levy, Basic Set Theory, Dover Publications, 2002. Note that viewed from the set.mm axiomatization, it is a metatheorem not formalizable in set.mm. It states: every formula in the language of FOL + + class terms, but without class variables, is provably equivalent (over {FOL, ax-ext, df-clab, df-cleq, df-clel }) to a formula in the language of FOL + (that is, without class terms).
The proof goes by induction on the complexity of the formula (see op. cit. for details). The base case is that of atomic formulas. The atomic formulas containing class terms are of one of the six following forms: for equality, , , , and for membership, , , . These cases are dealt with by eliminable-veqab, eliminable-abeqv, eliminable-abeqab, eliminable-velab, eliminable-abelv, eliminable-abelab respectively, which are all proved from {FOL, ax-ext, df-clab, df-cleq, df-clel }.
(Details on the proof of the above six theorems. To understand how they were systematically proved, look at the theorems "eliminablei" below, which are special instances of df-clab, dfcleq (proved from {FOL, ax-ext, df-cleq }), and dfclel (proved from {FOL, df-clel }). Indeed, denote by (i) the formula proved by "eliminablei". One sees that the RHS of (1) has no class terms, the RHS's of (2x) have only class terms of the form dealt with by (1), and the RHS's of (3x) have only class terms of the forms dealt with by (1) and (2a). Note that in order to prove eliminable2a, eliminable2b and eliminable3a, we need to substitute a class variable for a setvar variable. This is possible because setvars are class terms: this is the content of the syntactic theorem cv, which is used in these proofs (this does not appear in the html pages but it is in the set.mm file and you can check it using the Metamath program).)
The induction step relies on the fact that any formula is a FOL-combination of atomic formulas, so if one found equivalents for all atomic formulas constituting the formula, then the same FOL-combination of these equivalents will be equivalent to the original formula.
Note that one has a slightly more precise result: if the original formula has only class terms appearing in atomic formulas of the form , then df-clab is sufficient (over FOL) to eliminate class terms, and if the original formula has only class terms appearing in atomic formulas of the form and equalities, then df-clab, ax-ext and df-cleq are sufficient (over FOL) to eliminate class terms.
To prove that { df-clab, df-cleq, df-clel } provides a definitional extension of {FOL, ax-ext }, one needs to prove both the above Eliminability Theorem, which compares the expressive powers of the languages with and without class terms, and the Conservativity Theorem, which compares the deductive powers when one adds { df-clab, df-cleq, df-clel }. It states that a formula without class terms is provable in one axiom system if and only if it is provable in the other, and that this remains true when one adds further definitions to {FOL, ax-ext }. It is also proved in op. cit. The proof is more difficult, since one has to construct for each proof of a statement without class terms, an associated proof not using { df-clab, df-cleq, df-clel }. It involves a careful case study on the structure of the proof tree.