| Description: Extend wff definition to
include the membership connective between
classes.
For a general discussion of the theory of classes, see
https://us.metamath.org/mpeuni/mmset.html#class.
(The purpose of introducing wff
A ∈ B here
is to allow us to
express i.e. "prove" the wel 1711 of
predicate calculus in terms of the
wceq 1642 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 A and
B are introduced
temporarily for the purpose of this definition but
otherwise not used in predicate calculus. See df-clab 2340 for more
information on the set theory usage of wcel 1710.) | 