Theorem wl-dfcleq.just

Description: The hypotheses added to this version of df-cleq address the following:

1. Equality of classes is an equivalence relation, as expected of equality.

2. Equality of classes obeys the Law of Indiscernibles (Leibniz's Law), and is compatible with class membership.

3. Alpha-renaming is explicitly permitted.

(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)$$