Theorem wl-dfcleq.just

Description: Add more hypotheses, so equality of classes is an equivalence relation, does not conflict with properties (membership) of classes, and allows alpha-renaming. (Contributed by Wolf Lammen, 7-Apr-2026)

	Ref	Expression
Hypotheses	wl-dfcleq.just.1	$$⊢\forall x\left(x\in A\leftrightarrow x\in B\right)\leftrightarrow \forall y\left(y\in A\leftrightarrow y\in B\right)$$
	wl-dfcleq.just.id	$$⊢A=A$$
	wl-dfcleq.just.trans	$$⊢A=B\to \left(B=C\to C=A\right)$$
	wl-dfcleq.just.ax8	$$⊢A=B\to \left(A\in C\to B\in C\right)$$
	wl-dfcleq.just.ax9	$$⊢A=B\to \left(C\in A\to C\in B\right)$$
Assertion	wl-dfcleq.just	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-dfcleq.just.1	$$⊢\forall x\left(x\in A\leftrightarrow x\in B\right)\leftrightarrow \forall y\left(y\in A\leftrightarrow y\in B\right)$$
2		wl-dfcleq.just.id	$$⊢A=A$$
3		wl-dfcleq.just.trans	$$⊢A=B\to \left(B=C\to C=A\right)$$
4		wl-dfcleq.just.ax8	$$⊢A=B\to \left(A\in C\to B\in C\right)$$
5		wl-dfcleq.just.ax9	$$⊢A=B\to \left(C\in A\to C\in B\right)$$
6		wl-dfcleq.basic	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$