|Metamath Proof Explorer||
|Mirrors > Home > MPE Home > Th. List > df-clab||Unicode version|
|Description: Define class abstraction
notation (so-called 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 |
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 df-clab 2430, df-cleq 2436, and df-clel 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, 26-May-1993.)
|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 bj-hbab1 32291 bj-abbi 32296 bj-vjust 32307 eliminable1 32350 bj-vexwt 32365 bj-vexwvt 32367 bj-abfal 32409 bj-snsetex 32456|
|Copyright terms: Public domain||W3C validator|