**Description: **Extend wff definition to
include the membership connective between
classes.
(The purpose of introducing wff
*A* ∈ *B* here
is to allow us to
express i.e. "prove" the wel 1376 of
predicate calculus in terms of the
wceq 1228 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.) |