Description: Extend wff definition to
include the membership connective between
classes.
For a general discussion of the theory of classes, see
mmset.html#class.
(The purpose of introducing wff 𝐴 ∈ 𝐵 here is to allow us to
express i.e. "prove" the wel 1978 of
predicate calculus in terms of the
wcel 1977 of set theory, so that we don't
"overload" the ∈ connective
with two syntax definitions. This is done to prevent ambiguity that
would complicate some Metamath parsers. The class variables 𝐴 and
𝐵 are introduced temporarily for the
purpose of this definition but
otherwise not used in predicate calculus. See df-clab 2597 for more
information on the set theory usage of wcel 1977.) |