wel-wl - Mathbox for Wolf Lammen

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

Theorem wel-wl 33374

Description: Redefine

in a set context to avoid syntax check errors in mmj2.

and

must be distinct. (Contributed by Wolf Lammen, 27-Nov-2021.)

**Assertion**
Ref	Expression
wel-wl

**Proof of Theorem wel-wl**
Step	Hyp	Ref	Expression
1		wcel-wl 33373	1

Colors of variables: wff setvar class

Syntax hints:

wcel-wl 33373

This theorem is referenced by: (None)