Description: Define the equality
connective between classes. Definition 2.7 of
[Quine] p. 18. Also Definition 4.5 of
[TakeutiZaring] p. 13; Chapter 4
provides its justification and methods for eliminating it. Note that
its elimination will not necessarily result in a single wff in the
original language but possibly a "scheme" of wffs.
The hypotheses express that all instances of the conclusion where class
variables are replaced with setvar variables hold. Therefore, this
definition merely extends to class variables something that is true for
setvar variables, hence is conservative. This is only a proof sketch of
conservativity; for details see Appendix of [Levy] p. 357. This is the
reason why we call this axiomatic statement a "definition",
even though
it does not have the usual form of a definition. If we required a
definition to have the usual form, we would call df-cleq 2817 an axiom.
See also comments under df-clab 2803, df-clel 2896, and abeq2 2948.
In the form of dfcleq 2818, this is called the "axiom of
extensionality"
by [Levy] p. 338, who treats the theory of
classes as an extralogical
extension to our logic and set theory axioms.
While the three class definitions df-clab 2803, df-cleq 2817, and df-clel 2896
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
mmset.html#class 2896. (Contributed by NM, 15-Sep-1993.) (Revised
by BJ,
24-Jun-2019.) |