wcel2-wl - Mathbox for Wolf Lammen

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

Syntax Definition wcel2-wl 33375

Description: Redefine ∈ in a class context to avoid overloading and syntax check errors in mmj2. 𝑥 and 𝐵 may not be distinct.

**Hypotheses**
Ref	Expression
vx	setvar 𝑥
cB	class 𝐵

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

See definition df-wl-clelv2 33380 for more information.

Colors of variables: wff setvar class