| Description: Every class is equal to a
class abstraction (the class of sets belonging
to it). Theorem 5.2 of [Quine] p. 35.
This is a generalization to
classes of cvjust 2605. The proof does not rely on cvjust 2605, so cvjust 2605
could be proved as a special instance of it. Note however that abid1 2731
necessarily relies on df-clel 2606, whereas cvjust 2605 does not.
This theorem requires ax-ext 2590, df-clab 2597, df-cleq 2603, df-clel 2606, but
to prove that any specific class term not containing class variables is
a setvar or can be written as (is equal to) a class abstraction does not
require these $a-statements. This last fact is a metatheorem,
consequence of the fact that the only $a-statements with typecode
class
are cv 1474, cab 2596 and statements corresponding to
defined class
constructors.
Note on the simultaneous presence in set.mm of this abid1 2731 and its
commuted form abid2 2732: It is rare that two forms so closely
related
both appear in set.mm. Indeed, such equalities are generally used in
later proofs as parts of transitive inferences, and with the many
variants of eqtri 2632 (search for *eqtr*), it would be rare that
either
one would shorten a proof compared to the other. There is typically a
choice between (what we call) a "definitional form" where the
shorter
expression is on the lhs, and a "computational form" where the
shorter
expression is on the rhs. An example is df-2 10956
versus 1p1e2 11011. We do
not need 1p1e2 11011, but because it occurs "naturally"
in computations, it
can be useful to have it directly, together with a uniform set of
1-digit operations like 1p2e3 11029, etc. In most cases, we do not need
both a definitional and a computational forms. A definitional form
would favor consistency with genuine definitions, while a computationa
form is often more natural. The situation is similar with
biconditionals in propositional calculus: see for instance pm4.24 673 and
anidm 674, while other biconditionals generally appear
in a single form
(either definitional, but more often computational). In the present
case, the equality is important enough that both abid1 2731 and abid2 2732 are
in set.mm.
(Contributed by NM, 26-Dec-1993.) (Revised by BJ,
10-Nov-2020.) |
