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 ( y ) 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 3139 which is used, for example, to convert elirrv 7949 to elirr 7950. 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 2440, dfcleq 2446, and dfclel 2449 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 1369  . . 3 
3  wph  . . . 4  
4  vy  . . . 4  
5  3, 4  cab 2439  . . 3 
6  2, 5  wcel 1758  . 2 
7  3, 4, 1  wsb 1702  . 2 
8  6, 7  wb 184  1 
Colors of variables: wff setvar class 
This definition is referenced by: abid 2441 hbab1 2442 hbab 2444 cvjust 2448 abbiOLD 2586 cbvab 2595 cbvabOLD 2596 clelab 2598 clelabOLD 2599 nfabd2 2637 vjust 3082 dfsbcq2 3300 sbc8g 3305 unab 3731 inab 3732 difab 3733 csbab 3821 csbabgOLD 3822 exss 4672 iotaeq 5508 abrexex2g 6687 opabex3d 6688 opabex3 6689 abrexex2 6691 bjhbab1 33136 bjabbi 33141 bjvjust 33152 eliminable1 33195 bjvexwt 33210 bjvexwvt 33212 bjabfal 33254 bjsnsetex 33301 
Copyright terms: Public domain  W3C validator 