ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-clab GIF version

Definition df-clab 2069
Description: Define class abstraction notation (so-called by Quine), also called a "class builder" in the literature. 𝑥 and 𝑦 need not be distinct. Definition 2.1 of [Quine] p. 16. Typically, 𝜑 will have 𝑦 as a free variable, and "{𝑦𝜑} " is read "the class of all sets 𝑦 such that 𝜑(𝑦) is true." We do not define {𝑦𝜑} in isolation but only as part of an expression that extends or "overloads" the relationship.

This is our first use of the symbol to connect classes instead of sets. The syntax definition wcel 1434, which extends or "overloads" the wel 1435 definition connecting setvar variables, requires that both sides of be a class. In df-cleq 2075 and df-clel 2078, 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 setvar variable. Syntax definition cv 1284 allows us to substitute a setvar variable 𝑥 for a class variable: all sets are classes by cvjust 2077 (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 2188 for a quick overview).

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 called the "axiom of class comprehension" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. He calls the construction {𝑦𝜑} a "class term".

For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class. (Contributed by NM, 5-Aug-1993.)

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

Detailed syntax breakdown of Definition df-clab
StepHypRef Expression
1 vx . . . 4 setvar 𝑥
21cv 1284 . . 3 class 𝑥
3 wph . . . 4 wff 𝜑
4 vy . . . 4 setvar 𝑦
53, 4cab 2068 . . 3 class {𝑦𝜑}
62, 5wcel 1434 . 2 wff 𝑥 ∈ {𝑦𝜑}
73, 4, 1wsb 1686 . 2 wff [𝑥 / 𝑦]𝜑
86, 7wb 103 1 wff (𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
Colors of variables: wff set class
This definition is referenced by:  abid  2070  hbab1  2071  hbab  2073  cvjust  2077  abbi  2193  sb8ab  2201  cbvab  2202  clelab  2204  nfabd  2238  vjust  2603  dfsbcq2  2819  sbc8g  2823  csbabg  2964  unab  3238  inab  3239  difab  3240  rabeq0  3281  abeq0  3282  oprcl  3602  exss  3990  peano1  4343  peano2  4344  iotaeq  4905  nfvres  5238  abrexex2g  5778  opabex3d  5779  opabex3  5780  abrexex2  5782  bdab  10787  bdph  10799  bdcriota  10832
  Copyright terms: Public domain W3C validator