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	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
	wl-dfcleq.just.id	⊢ 𝐴 = 𝐴
	wl-dfcleq.just.trans	⊢ ( 𝐴 = 𝐵 → ( 𝐵 = 𝐶 → 𝐶 = 𝐴 ) )
	wl-dfcleq.just.ax8	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝐶 → 𝐵 ∈ 𝐶 ) )
	wl-dfcleq.just.ax9	⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
Assertion	wl-dfcleq.just	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		wl-dfcleq.just.1	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
2		wl-dfcleq.just.id	⊢ 𝐴 = 𝐴
3		wl-dfcleq.just.trans	⊢ ( 𝐴 = 𝐵 → ( 𝐵 = 𝐶 → 𝐶 = 𝐴 ) )
4		wl-dfcleq.just.ax8	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝐶 → 𝐵 ∈ 𝐶 ) )
5		wl-dfcleq.just.ax9	⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
6		wl-dfcleq.basic	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )