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	wff 𝑥 ∈ 𝑦

Proof of Theorem wel-wl

Step	Hyp	Ref	Expression
1		wcel-wl 33373	1 wff 𝑥 ∈ 𝑦

Syntax hints:   ∈ wcel-wl 33373

This theorem is referenced by: (None)