Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable (that has a free variable ) to a theorem with a class variable , we substitute for throughout and simplify, where is a new class variable not already in the wff. An example is the conversion of zfauscl 2700 to inex1 2711 (look at the instance of zfauscl 2700 that occurs in the proof of inex1 2711). Conversely, to convert a theorem with a class variable to one with , we substitute for throughout and simplify, where and are new set and wff variables not already in the wff. An example is cp 4702, which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 4701.