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	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) )
2		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
3	1 2	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
4	3	cbvexvw	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
5	4	wl-dfclel.just	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) )