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

Definition df-clab 2000
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 1366, which extends or "overloads" the wel 1367 definition connecting setvar variables, requires that both sides of be a class. In df-cleq 2006 and df-clel 2009, 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 1222 allows us to substitute a setvar variable for a class variable: all sets are classes by cvjust 2008 (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 2119 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 1222 . . 3
3 wph . . . 4
4 vy . . . 4  setvar
53, 4cab 1999 . . 3  {  |  }
62, 5wcel 1366 . 2  {  |  }
73, 4, 1wsb 1618 . 2
86, 7wb 98 1  {  |  }
Colors of variables: wff set class
This definition is referenced by:  abid  2001  hbab1  2002  hbab  2004  cvjust  2008  abbi  2124  sb8ab  2132  cbvab  2133  clelab  2135  nfabd  2169  vjust  2527  dfsbcq2  2735  sbc8g  2739  csbabg  2875  unab  3172  inab  3173  difab  3174  rabeq0  3215  abeq0  3216  oprcl  3536  exss  3926  peano1  4232  peano2  4233  iotaeq  4790  nfvres  5119  abrexex2g  5658  opabex3d  5659  opabex3  5660  abrexex2  5662  bdab  8223  bdph  8235  bdcriota  8268
  Copyright terms: Public domain W3C validator