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-cleq2482 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq2482 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with set variables (see cleljust2113), so we don't include any
set theory axiom as a hypothesis. See also comments about the syntax
under df-clab2476. Alternate definitions of (but that require
either or to be a set) are shown by clel23134, clel33136, and
clel43137.

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.