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 3167 which is used, for example, to convert elirrv 8044 to elirr 8045. 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 2443, dfcleq 2449, and dfclel 2452 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 1394  . . 3 
3  wph  . . . 4  
4  vy  . . . 4  
5  3, 4  cab 2442  . . 3 
6  2, 5  wcel 1818  . 2 
7  3, 4, 1  wsb 1739  . 2 
8  6, 7  wb 184  1 
Colors of variables: wff setvar class 
This definition is referenced by: abid 2444 hbab1 2445 hbab 2447 cvjust 2451 abbiOLD 2589 cbvab 2598 cbvabOLD 2599 clelab 2601 clelabOLD 2602 nfabd2 2640 vjust 3110 dfsbcq2 3330 sbc8g 3335 unab 3764 inab 3765 difab 3766 csbab 3855 csbabgOLD 3856 exss 4715 iotaeq 5564 abrexex2g 6777 opabex3d 6778 opabex3 6779 abrexex2 6781 bjhbab1 34356 bjabbi 34361 bjvjust 34372 eliminable1 34415 bjvexwt 34430 bjvexwvt 34432 bjabfal 34474 bjsnsetex 34521 
Copyright terms: Public domain  W3C validator 