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 3008 which is used, for example, to convert elirrv 7759 to elirr 7760. 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 3 class definitions dfclab 2409, dfcleq 2415, and dfclel 2418 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, 5Aug1993.) 
Ref  Expression 

dfclab 
Step  Hyp  Ref  Expression 

1  vx  . . . 4  
2  1  cv 1686  . . 3 
3  wph  . . . 4  
4  vy  . . . 4  
5  3, 4  cab 2408  . . 3 
6  2, 5  wcel 1749  . 2 
7  3, 4, 1  wsb 1693  . 2 
8  6, 7  wb 178  1 
Colors of variables: wff setvar class 
This definition is referenced by: abid 2410 hbab1 2411 hbab 2413 cvjust 2417 abbi 2532 cbvab 2540 clelab 2542 nfabd2 2576 vjust 2952 dfsbcq2 3167 sbc8g 3171 unab 3594 inab 3595 difab 3596 csbab 3684 csbabgOLD 3685 exss 4527 iotaeq 5361 abrexex2g 6523 opabex3d 6524 opabex3 6525 abrexex2 6527 bjhbab1 31787 bjabbi 31792 bjvjust 31802 bjvexwt 31842 bjvexwv 31844 bjsnsetex 31903 
Copyright terms: Public domain  W3C validator 