| 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 to prove the
wel 2146 of predicate calculus in terms of the wcel 2145
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 2739 for more information on
the set theory usage of wcel 2145. | 