| 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 1377 of
predicate calculus in terms of the
wceq 1374 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.) |
