Theorem wl-dfclel

Description: The defining characterization of class membership. Unlike the forms on which it is based, it is unrestricted. Proven in Tarski's FOL, from the axiom of (set) extensionality ( ax-ext ), the definitions df-clel and df-cleq . (Contributed by BJ, 27-Jun-2019) Base on wl-dfclel.just . (Revised by Wolf Lammen, 13-Apr-2026)

	Ref	Expression
Assertion	wl-dfclel	$$⊢A\in B\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢x=y\to \left(x=A\leftrightarrow y=A\right)$$
2		eleq1w	$$⊢x=y\to \left(x\in B\leftrightarrow y\in B\right)$$
3	1 2	anbi12d	$$⊢x=y\to \left(\left(x=A\wedge x\in B\right)\leftrightarrow \left(y=A\wedge y\in B\right)\right)$$
4	3	cbvexvw	$$⊢\exists x\left(x=A\wedge x\in B\right)\leftrightarrow \exists y\left(y=A\wedge y\in B\right)$$
5	4	wl-dfclel.just	$$⊢A\in B\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$