Description: Define the membership
connective between classes. Theorem 6.3 of
[Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we
adopt as a definition. See these references for its metalogical
justification. Note that like df-cleq2449 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq2449 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust2109), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab2443. Alternate definitions of (but that
require either or to be a set) are shown by clel23236,
clel33238, and clel43239.
This is called the "axiom of membership" 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-clab2443, df-cleq2449, and df-clel2452
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.
