Theorem wl-dfclel.just

Description: Add a hypotheses to wl-dfclel.basic , that allows alpha-renaming. (Contributed by Wolf Lammen, 7-Apr-2026)

	Ref	Expression
Hypothesis	wl-dfclel.just.1	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
Assertion	wl-dfclel.just	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		wl-dfclel.just.1	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
2		wl-dfclel.basic	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) )