wcel-wl - Mathbox for Wolf Lammen

	Mathbox for Wolf Lammen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > wcel-wl		Structured version Visualization version Unicode version

Syntax Definition wcel-wl 33373

Description: Redefine

in a class context to avoid overloading and syntax check errors in mmj2. This operator requires

and

distinct.

**Hypotheses**
Ref	Expression
vx
cB

**Assertion**
Ref	Expression
wcel-wl

This syntax is primitive. The first axiom using it is ax-wl-8cl 33377.

Colors of variables: wff setvar class