This section introduces class equality in df-cleq.
Note that apart from the local introduction of class variables to state the
syntax axioms wceq and wcel, this section is the first to use class
variables. Therefore, the file set.mm contains declarations of class
variables at the beginning of this section (not visible on the webpages).