Theorem wel2-wl 33376

Description: Redefine ∈ in a set context to avoid syntax check errors in mmj2. It is no syntactic error to assign the same variable to 𝑥 and 𝑦. (Contributed by Wolf Lammen, 27-Nov-2021.)

Assertion

Ref	Expression
wel2-wl	wff 𝑥 ∈ 𝑦

Proof of Theorem wel2-wl

Step	Hyp	Ref	Expression
1		wcel2-wl 33375	1 wff 𝑥 ∈ 𝑦

Syntax hints:   ∈ wcel2-wl 33375

This theorem is referenced by: (None)