**Description: **Extend wff notation to
include the proper substitution of a class for a
set. Read this notation as "the proper substitution of class for
set variable
in wff ."
(The purpose of introducing here is to allow us to
express i.e. "prove" the wsb 1605 of
predicate calculus in terms of the
wsbc 1604 of set theory, so that we don't
"overload" its connectives with
two syntax definitions. This is done to prevent ambiguity that would
complicate some Metamath parsers. The class variable is
introduced temporarily for the purpose of this definition but otherwise
not used in predicate calculus.) |