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	$$⊢\exists x\left(x=A\wedge x\in B\right)\leftrightarrow \exists y\left(y=A\wedge y\in B\right)$$
Assertion	wl-dfclel.just	$$⊢A\in B\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-dfclel.just.1	$$⊢\exists x\left(x=A\wedge x\in B\right)\leftrightarrow \exists y\left(y=A\wedge y\in B\right)$$
2		wl-dfclel.basic	$$⊢A\in B\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$