Theorem wl-dfclel

Description: Characterization of the elements of a class. (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)$$