Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfclab  Unicode version 
Description: Define class abstraction
notation (socalled 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 e. relationship.
This is our first use of the 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 done with theorems such as vtoclg 3030 which is used, for example, to convert elirrv 7812 to elirr 7813. 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". While the three class definitions dfclab 2430, dfcleq 2436, and dfclel 2439 are eliminable and conservative and thus meet the requirements for sound definitions, they are technically axioms in that they do not satisfy the requirements for the current definition checker. The proofs of conservativity require external justification that is beyond the scope of the definition checker. For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class. (Contributed by NM, 26May1993.) 
Ref  Expression 

dfclab 
Step  Hyp  Ref  Expression 

1  vx  . . . 4  
2  1  cv 1368  . . 3 
3  wph  . . . 4  
4  vy  . . . 4  
5  3, 4  cab 2429  . . 3 
6  2, 5  wcel 1756  . 2 
7  3, 4, 1  wsb 1700  . 2 
8  6, 7  wb 184  1 
Colors of variables: wff setvar class 
This definition is referenced by: abid 2431 hbab1 2432 hbab 2434 cvjust 2438 abbi 2553 cbvab 2561 clelab 2563 nfabd2 2597 vjust 2973 dfsbcq2 3189 sbc8g 3194 unab 3617 inab 3618 difab 3619 csbab 3707 csbabgOLD 3708 exss 4555 iotaeq 5389 abrexex2g 6554 opabex3d 6555 opabex3 6556 abrexex2 6558 bjhbab1 32291 bjabbi 32296 bjvjust 32307 eliminable1 32350 bjvexwt 32365 bjvexwvt 32367 bjabfal 32409 bjsnsetex 32456 
Copyright terms: Public domain  W3C validator 