Theorem wl-dfcleq.just 37837

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.)

Hypotheses

Ref	Expression
wl-dfcleq.just.1	⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
wl-dfcleq.just.id	⊢ 𝐴 = 𝐴
wl-dfcleq.just.trans	⊢ (𝐴 = 𝐵 → (𝐵 = 𝐶 → 𝐶 = 𝐴))
wl-dfcleq.just.ax8	⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 → 𝐵 ∈ 𝐶))
wl-dfcleq.just.ax9	⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Assertion

Ref	Expression
wl-dfcleq.just	⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑦)

Proof of Theorem wl-dfcleq.just

Step	Hyp	Ref	Expression
1		wl-dfcleq.basic 37836	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  wl-dfcleq  37841