| Description: Extend wff definition to
include the membership connective between
classes.
(The purpose of introducing wff 𝐴 ∈ 𝐵 here is to allow us to
express i.e. "prove" the wel 1464 of
predicate calculus in terms of the
wceq 1314 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 𝐴 and
𝐵 are introduced temporarily for the
purpose of this definition but
otherwise not used in predicate calculus.) |
