Syntax Definition wcel 1092

Description: Extend wff definition to include the membership connective between classes.

Hypotheses

Ref	Expression
cA	class A
cB	class B

Assertion

Ref	Expression
wcel	wff A ∈ B

See definition df-clab 1093 for more information.

metamath.org