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

Definition df-clab 2127
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,  ph will have  y as a free variable, and " { y  |  ph } " is read "the class of all sets  y such that  ph ( y ) is true." We do not define  { y  |  ph } in isolation but only as part of an expression that extends or "overloads" the  e. relationship.

This is our first use of the 
e. symbol to connect classes instead of sets. The syntax definition wcel 1481, which extends or "overloads" the wel 1482 definition connecting setvar variables, requires that both sides of  e. be a class. In df-cleq 2133 and df-clel 2136, we introduce a new kind of variable (class variable) that can substituted with expressions such as  { y  | 
ph }. In the present definition, the  x on the left-hand side is a setvar variable. Syntax definition cv 1331 allows us to substitute a setvar variable  x for a class variable: all sets are classes by cvjust 2135 (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 2249 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  |  ph } a "class term".

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

Assertion
Ref Expression
df-clab  |-  ( x  e.  { y  | 
ph }  <->  [ x  /  y ] ph )

Detailed syntax breakdown of Definition df-clab
StepHypRef Expression
1 vx . . . 4  setvar  x
21cv 1331 . . 3  class  x
3 wph . . . 4  wff  ph
4 vy . . . 4  setvar  y
53, 4cab 2126 . . 3  class  { y  |  ph }
62, 5wcel 1481 . 2  wff  x  e. 
{ y  |  ph }
73, 4, 1wsb 1736 . 2  wff  [ x  /  y ] ph
86, 7wb 104 1  wff  ( x  e.  { y  | 
ph }  <->  [ x  /  y ] ph )
Colors of variables: wff set class
This definition is referenced by:  abid  2128  hbab1  2129  hbab  2131  cvjust  2135  abbi  2254  sb8ab  2262  cbvabw  2263  cbvab  2264  clelab  2266  nfabd  2301  vjust  2690  dfsbcq2  2915  sbc8g  2919  csbabg  3065  unab  3347  inab  3348  difab  3349  rabeq0  3396  abeq0  3397  oprcl  3736  exss  4156  peano1  4515  peano2  4516  iotaeq  5103  nfvres  5461  abrexex2g  6025  opabex3d  6026  opabex3  6027  abrexex2  6029  bdab  13205  bdph  13217  bdcriota  13250
  Copyright terms: Public domain W3C validator