| 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 prove
the wel 2168 of predicate calculus in terms of the wceq 1364
of set theory, so
that we do not 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 2183 for more information on
the set theory usage of wcel 2167. | 