Definition df-wl-clelv2 33380

Description: Define the term 𝑥 ∈ 𝐴, 𝑥 in 𝐴 permitted. (Contributed by Wolf Lammen, 27-Nov-2021.)

Assertion

Ref	Expression
df-wl-clelv2	⊢ (𝑥 ∈ 𝐴 ↔ ∀𝑢(𝑢 = 𝑥 → 𝑢 ∈ 𝐴))

Distinct variable groups:   𝑢,𝐴   𝑥,𝑢

Allowed substitution hint:   𝐴(𝑥)

Detailed syntax breakdown of Definition df-wl-clelv2

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3	1, 2	wcel2-wl 33375	. 2 wff 𝑥 ∈ 𝐴
4		vu	. . . . 5 setvar 𝑢
5	4, 1	weq 1874	. . . 4 wff 𝑢 = 𝑥
6	4, 2	wcel-wl 33373	. . . 4 wff 𝑢 ∈ 𝐴
7	5, 6	wi 4	. . 3 wff (𝑢 = 𝑥 → 𝑢 ∈ 𝐴)
8	7, 4	wal 1481	. 2 wff ∀𝑢(𝑢 = 𝑥 → 𝑢 ∈ 𝐴)
9	3, 8	wb 196	1 wff (𝑥 ∈ 𝐴 ↔ ∀𝑢(𝑢 = 𝑥 → 𝑢 ∈ 𝐴))

This definition is referenced by:  wl-ax8clv2  33381