Definition df-clab 2717

Description: Define class abstractions, that is, classes of the form {𝑦 ∣ 𝜑}, which is read "the class of sets 𝑦 such that 𝜑(𝑦)".

A few remarks are in order:

1. The axiomatic statement df-clab 2717 does not define the class abstraction {𝑦 ∣ 𝜑} itself, that is, it does not have the form ⊢ {𝑦 ∣ 𝜑} = ... 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 df-cleq 2731). Instead, df-clab 2717 has the form ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ ...), 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 df-clab 2717 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 ax-ext 2710. Therefore, df-clab 2717 can be considered a definition only in systems that can prove ax-ext 2710 (and the necessary first-order logic).

2. As in all definitions, the definiendum (the left-hand side of the biconditional) has no disjoint variable conditions. In particular, the setvar variables 𝑥 and 𝑦 need not be distinct, and the formula 𝜑 may depend on both 𝑥 and 𝑦. This is necessary, as with all definitions, since if there was for instance a disjoint variable condition on 𝑥, 𝑦, then one could not do anything with expressions like 𝑥 ∈ {𝑥 ∣ 𝜑} which are sometimes useful to shorten proofs (because of abid 2720). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑.

3. Remark 1 stresses that df-clab 2717 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 ∈ has already appeared earlier (e.g., in the non-syntactic statement ax-8 2114). Indeed, the definiendum extends, or "overloads", the membership predicate ∈ from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This is possible because of wcel 2112 and cab 2716, and it can be called an "extension" of the membership predicate because of wel 2113, whose proof uses cv 1542. An a posteriori justification for cv 1542 is given by cvjust 2733, 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 3711).

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 3496 which is used, for example, to convert elirrv 9260 to elirr 9261.

5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2717, df-cleq 2731, and df-clel 2818, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 28640), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2731 and df-clel 2818). 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, object-level) conservative extension of FOL= plus ax-ext 2710, 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 {𝑦 ∣ 𝜑} 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 2872 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2872. (Contributed by NM, 26-May-1993.) (Revised by BJ, 19-Aug-2023.)

Assertion

Ref	Expression
df-clab	⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

Detailed syntax breakdown of Definition df-clab

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar 𝑥
2	1	cv 1542	. . 3 class 𝑥
3		wph	. . . 4 wff 𝜑
4		vy	. . . 4 setvar 𝑦
5	3, 4	cab 2716	. . 3 class {𝑦 ∣ 𝜑}
6	2, 5	wcel 2112	. 2 wff 𝑥 ∈ {𝑦 ∣ 𝜑}
7	3, 4, 1	wsb 2072	. 2 wff [𝑥 / 𝑦]𝜑
8	6, 7	wb 209	1 wff (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

This definition is referenced by:  eleq1ab  2718  abid  2720  vexwt  2721  vexw  2722  nfsab1  2724  hbab1OLD  2726  hbab  2727  hbabg  2728  cvjust  2733  abbi1  2808  abbi  2812  cbvabv  2813  cbvabw  2814  cbvabwOLD  2815  cbvab  2816  abeq2w  2817  abbi2dv  2877  clelab  2883  clelabOLD  2884  nfabdw  2930  nfabdwOLD  2931  nfabd  2932  rabrabi  3418  abv  3434  abvALT  3435  elab6g  3594  elrabi  3612  ralab  3622  dfsbcq2  3715  sbc8g  3720  sbcimdv  3787  sbcg  3792  csbied  3867  ss2abdv  3994  ss2abdvALT  3995  unabw  4229  unab  4230  inab  4231  difab  4232  notabw  4235  noel  4262  noelOLD  4263  vn0  4270  eq0  4275  ab0w  4305  ab0OLD  4307  ab0orv  4310  eq0rdv  4336  csbab  4369  disj  4379  rzal  4437  ralf0  4442  exss  5371  iotaeq  6386  abrexex2g  7777  opabex3d  7778  opabex3rd  7779  opabex3  7780  xpab  33554  eliminable1  34945  eliminable-velab  34951  bj-ab0  34995  bj-elabd2ALT  35015  bj-gabima  35030  bj-snsetex  35055  wl-clabv  35652  wl-clabtv  35654  wl-clabt  35655  elabgw  40065  scottabf  41720