Definition df-wl-clelv2 33380

Description: Define the term x e. A, x in A permitted. (Contributed by Wolf Lammen, 27-Nov-2021.)

Assertion

Ref	Expression
df-wl-clelv2	|- ( x e. A <-> A. u ( u = x -> u e. A ) )

Distinct variable groups:   u, A   x, u

Allowed substitution hint:   A( x)

Detailed syntax breakdown of Definition df-wl-clelv2

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		cA	. . 3 class A
3	1, 2	wcel2-wl 33375	. 2 wff x e. A
4		vu	. . . . 5 setvar u
5	4, 1	weq 1874	. . . 4 wff u = x
6	4, 2	wcel-wl 33373	. . . 4 wff u e. A
7	5, 6	wi 4	. . 3 wff ( u = x -> u e. A )
8	7, 4	wal 1481	. 2 wff A. u ( u = x -> u e. A )
9	3, 8	wb 196	1 wff ( x e. A <-> A. u ( u = x -> u e. A ) )

This definition is referenced by:  wl-ax8clv2  33381