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

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