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 GIF 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	setvar 𝑥
cB	class 𝐵

**Assertion**
Ref	Expression
wcel-wl	wff 𝑥 ∈ 𝐵

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

Colors of variables: wff setvar class