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

Definition df-clab 2005
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 1370, which extends or "overloads" the wel 1371 definition connecting setvar variables, requires that both sides of be a class. In df-cleq 2011 and df-clel 2014, 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 1225 allows us to substitute a setvar variable for a class variable: all sets are classes by cvjust 2013 (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 2124 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 1225 . . 3
3 wph . . . 4
4 vy . . . 4  setvar
53, 4cab 2004 . . 3  {  |  }
62, 5wcel 1370 . 2  {  |  }
73, 4, 1wsb 1623 . 2
86, 7wb 98 1  {  |  }
Colors of variables: wff set class
This definition is referenced by:  abid  2006  hbab1  2007  hbab  2009  cvjust  2013  abbi  2129  sb8ab  2137  cbvab  2138  clelab  2140  nfabd  2174  vjust  2532  dfsbcq2  2740  sbc8g  2744  csbabg  2880  unab  3177  inab  3178  difab  3179  rabeq0  3220  abeq0  3221  oprcl  3543  exss  3933  peano1  4240  peano2  4241  iotaeq  4798  nfvres  5127  abrexex2g  5666  opabex3d  5667  opabex3  5668  abrexex2  5670  bdab  7257  bdph  7269  bdcriota  7302
  Copyright terms: Public domain W3C validator