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	|- ( A. x ( x e. A <-> x e. B ) <-> A. y ( y e. A <-> y e. B ) )
	wl-dfcleq.just.id	|- A = A
	wl-dfcleq.just.trans	|- ( A = B -> ( B = C -> C = A ) )
	wl-dfcleq.just.ax8	|- ( A = B -> ( A e. C -> B e. C ) )
	wl-dfcleq.just.ax9	|- ( A = B -> ( C e. A -> C e. B ) )
Assertion	wl-dfcleq.just	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Proof

Step	Hyp	Ref	Expression
1		wl-dfcleq.just.1	|- ( A. x ( x e. A <-> x e. B ) <-> A. y ( y e. A <-> y e. B ) )
2		wl-dfcleq.just.id	|- A = A
3		wl-dfcleq.just.trans	|- ( A = B -> ( B = C -> C = A ) )
4		wl-dfcleq.just.ax8	|- ( A = B -> ( A e. C -> B e. C ) )
5		wl-dfcleq.just.ax9	|- ( A = B -> ( C e. A -> C e. B ) )
6		wl-dfcleq.basic	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )