This is our first use of the symbol to connect classes instead of sets. The syntax definition wcel 956, which extends or "overloads" the wel 957 definition connecting set variables, requires that both sides of be a class. In df-cleq 1467 and df-clel 1470, we introduce a new kind of variable (class variable) that can substituted with expressions such as . In the present definition, the on the left-hand side is a set variable. Syntax definition cv 953 allows us to substitute a set variable for a class variable: all sets are classes by cvjust 1469 (but not necessarily vice-versa). For a full description of how classes are introduced and how to recover the primitive language, see the discussion in Quine (and under abeq2 1565 for a quick overview).

Because class variables can be substituted with compound expressions and set variables cannot, it is often useful to convert a theorem containing a free set variable to a more general version with a class variable. This is done with theorems such as vtoclg 1843 which is used, for example, to convert elirrv 4578 to elirr 4579.