Description: Define class abstractions, that is, classes of the form { y  ph } , which is read "the class of sets y such that ph ( y ) ".
A few remarks are in order:
1. The axiomatic statement dfclab does not define the class abstraction { y  ph } itself, that is, it does not have the form  { y  ph } = ... that a standard definition should have (for a good reason: equality itself has not yet been defined or axiomatized for class abstractions; it is defined later in dfcleq ). Instead, dfclab has the form  ( x e. { y  ph } <> ... ) , meaning that it only defines what it means for a setvar to be a member of a class abstraction. As a consequence, one can say that dfclab defines class abstractions if and only if a class abstraction is completely determined by which elements belong to it, which is the content of the axiom of extensionality axext . Therefore, dfclab can be considered a definition only in systems that can prove axext (and the necessary firstorder logic).
2. As in all definitions, the definiendum (the lefthand side of the biconditional) has no disjoint variable conditions. In particular, the setvar variables x and y need not be distinct, and the formula ph may depend on both x and y . This is necessary, as with all definitions, since if there was for instance a disjoint variable condition on x , y , then one could not do anything with expressions like x e. { x  ph } which are sometimes useful to shorten proofs (because of abid ). Most often, however, x does not occur in { y  ph } and y is free in ph .
3. Remark 1 stresses that dfclab does not have the standard form of a definition for a class, but one could be led to think it has the standard form of a definition for a formula. However, it also fails that test since the membership predicate e. has already appeared earlier (e.g., in the nonsyntactic statement ax8 ). Indeed, the definiendum extends, or "overloads", the membership predicate e. from formulas of the form "setvar e. setvar" to formulas of the form "setvar e. class abstraction". This is possible because of wcel and cab , and it can be called an "extension" of the membership predicate because of wel , whose proof uses cv . An a posteriori justification for cv is given by cvjust , stating that every setvar can be written as a class abstraction (though conversely not every class abstraction is a set, as illustrated by Russell's paradox ru ).
4. Proof techniques. Because class variables can be substituted with compound expressions and setvar variables cannot, it is often useful to convert a theorem containing a free setvar variable to a more general version with a class variable. This is done with theorems such as vtoclg which is used, for example, to convert elirrv to elirr .
5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, dfclab , dfcleq , and dfclel , to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions ), they are not definitions (see Remarks 1 and 3 above, and similarly for dfcleq and dfclel ). One could be less strict and decide to call "definition" every axiomatic statement which provides an eliminable and conservative extension of the considered axiom system. But the notion of conservativity may be given two different meanings in set.mm, due to the difference between the "scheme level" of set.mm and the "object level" of classical treatments. For a proof that these three axiomatic statements yield an eliminable and weakly (that is, objectlevel) conservative extension of FOL= plus axext , see Appendix of Levy p. 357.
6. References and history. The concept of class abstraction dates back to at least Frege, and is used by Whitehead and Russell. This definition is Definition 2.1 of Quine p. 16 and Axiom 4.3.1 of Levy p. 12. It is called the "axiom of class comprehension" by Levy p. 358, who treats the theory of classes as an extralogical extension to predicate logic and set theory axioms. He calls the construction { y  ph } a "class term". For a full description of how classes are introduced and how to recover the primitive language, see the books of Quine and Levy (and the comment of abeq2 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class . (Contributed by NM, 26May1993) (Revised by BJ, 19Aug2023)
Ref  Expression  

Assertion  dfclab   ( x e. { y  ph } <> [ x / y ] ph ) 
Step  Hyp  Ref  Expression 

0  vx   x 

1  0  cv   x 
2  vy   y 

3  wph   ph 

4  3 2  cab   { y  ph } 
5  1 4  wcel   x e. { y  ph } 
6  3 2 0  wsb   [ x / y ] ph 
7  5 6  wb   ( x e. { y  ph } <> [ x / y ] ph ) 