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

Definition df-clab 2001
Description: Define class abstraction notation (so-called by Quine), also called a "class builder" in the literature. x and y need not be distinct. Definition 2.1 of [Quine] p. 16. Typically, φ will have y as a free variable, and "{yφ} " is read "the class of all sets y such that φ(y) is true." We do not define {yφ} 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 1367, which extends or "overloads" the wel 1368 definition connecting setvar variables, requires that both sides of be a class. In df-cleq 2007 and df-clel 2010, we introduce a new kind of variable (class variable) that can substituted with expressions such as {yφ}. In the present definition, the x on the left-hand side is a setvar variable. Syntax definition cv 1223 allows us to substitute a setvar variable x for a class variable: all sets are classes by cvjust 2009 (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 2120 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 {yφ} 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 (x {yφ} ↔ [x / y]φ)

Detailed syntax breakdown of Definition df-clab
StepHypRef Expression
1 vx . . . 4 setvar x
21cv 1223 . . 3 class x
3 wph . . . 4 wff φ
4 vy . . . 4 setvar y
53, 4cab 2000 . . 3 class {yφ}
62, 5wcel 1367 . 2 wff x {yφ}
73, 4, 1wsb 1619 . 2 wff [x / y]φ
86, 7wb 98 1 wff (x {yφ} ↔ [x / y]φ)
Colors of variables: wff set class
This definition is referenced by:  abid  2002  hbab1  2003  hbab  2005  cvjust  2009  abbi  2125  sb8ab  2133  cbvab  2134  clelab  2136  nfabd  2170  vjust  2528  dfsbcq2  2736  sbc8g  2740  csbabg  2876  unab  3173  inab  3174  difab  3175  rabeq0  3216  abeq0  3217  oprcl  3537  exss  3927  peano1  4233  peano2  4234  iotaeq  4791  nfvres  5120  abrexex2g  5659  opabex3d  5660  opabex3  5661  abrexex2  5663  bdab  8295  bdph  8307  bdcriota  8340
  Copyright terms: Public domain W3C validator