Syntax Definition wcel 956

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

(The purpose of introducing wff A ∈ B here is to allow us to express i.e. "prove" the wel 957 of predicate calculus in terms of the wceq 954 of set theory, so that we don't "overload" the ∈ connective with two syntax definitions. This is done to prevent ambiguity that causes problems in some Metamath parsers. The class variables A and B are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-clab 1462 for more information on the set theory usage of wcel 956.)

Hypotheses

Ref	Expression
wcel.cA	class A
wcel.cB	class B

Assertion

Ref	Expression
wcel	wff A ∈ B

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

Copyright terms: Public domain