(The purpose of introducing wffAe.B here is to allow us to
express i.e. "prove" the wel1759 of
predicate calculus in terms of the
wcel1758 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-clab2440 for more
information on the set theory usage of wcel1758.)

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-81760.