Theorem wl-dfcleq.just 37873

Description: The hypotheses added to this version of df-cleq 2732 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.)

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 37872	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  wl-dfcleq  37877