(The purpose of introducing wffAe.B here is to allow us to
express i.e. "prove" the wel1733 of
predicate calculus in terms of the
wcel1732 of set theory, so that we don't
"overload" the e. 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. See df-clab2476 for more
information on the set theory usage of wcel1732.)

Hypotheses

Ref

Expression

wcel.cA

No typesetting for: class A

wcel.cB

No typesetting for: class B

Assertion

Ref

Expression

wcel

No typesetting for: wff A e. B

This syntax is primitive. The first axiom using it is ax-81734.