Metamath Proof Explorer

Theorem wl-dfcleq

Description: The defining characterization of class equality. This version of df-cleq has no restrictions, unlike the forms on which it is based. It is proved in Tarski's FOL from the axiom of extensionality ( ax-ext ), the definition of class equality ( df-cleq ), and the definition of class membership ( df-clel ).

Its forward implication is known as "class extensionality". (Contributed by NM, 15-Sep-1993) (Revised by BJ, 24-Jun-2019) Base on wl-dfcleq.just . (Revised by Wolf Lammen, 7-Apr-2026)

Ref Expression
Assertion wl-dfcleq ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B

Proof

Step Hyp Ref Expression
1 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
2 eleq1w ⊢ x = y → x ∈ B ↔ y ∈ B
3 1 2 bibi12d ⊢ x = y → x ∈ A ↔ x ∈ B ↔ y ∈ A ↔ y ∈ B
4 3 cbvalvw ⊢ ∀ x x ∈ A ↔ x ∈ B ↔ ∀ y y ∈ A ↔ y ∈ B
5 eqid ⊢ A = A
6 eqtr ⊢ A = B ∧ B = C → A = C
7 6 eqcomd ⊢ A = B ∧ B = C → C = A
8 7 ex ⊢ A = B → B = C → C = A
9 eqeq2 ⊢ A = B → x = A ↔ x = B
10 9 biimpd ⊢ A = B → x = A → x = B
11 10 anim1d ⊢ A = B → x = A ∧ x ∈ C → x = B ∧ x ∈ C
12 11 eximdv ⊢ A = B → ∃ x x = A ∧ x ∈ C → ∃ x x = B ∧ x ∈ C
13 dfclel ⊢ A ∈ C ↔ ∃ x x = A ∧ x ∈ C
14 dfclel ⊢ B ∈ C ↔ ∃ x x = B ∧ x ∈ C
15 12 13 14 3imtr4g ⊢ A = B → A ∈ C → B ∈ C
16 wl-dfcleq.basic ⊢ A = B ↔ ∀ y y ∈ A ↔ y ∈ B
17 biimp ⊢ y ∈ A ↔ y ∈ B → y ∈ A → y ∈ B
18 17 alimi ⊢ ∀ y y ∈ A ↔ y ∈ B → ∀ y y ∈ A → y ∈ B
19 1 biimpd ⊢ x = y → x ∈ A → y ∈ A
20 19 eqcoms ⊢ y = x → x ∈ A → y ∈ A
21 eleq1w ⊢ y = x → y ∈ B ↔ x ∈ B
22 21 biimpd ⊢ y = x → y ∈ B → x ∈ B
23 20 22 imim12d ⊢ y = x → y ∈ A → y ∈ B → x ∈ A → x ∈ B
24 23 spimvw ⊢ ∀ y y ∈ A → y ∈ B → x ∈ A → x ∈ B
25 18 24 syl ⊢ ∀ y y ∈ A ↔ y ∈ B → x ∈ A → x ∈ B
26 16 25 sylbi ⊢ A = B → x ∈ A → x ∈ B
27 26 anim2d ⊢ A = B → x = C ∧ x ∈ A → x = C ∧ x ∈ B
28 27 eximdv ⊢ A = B → ∃ x x = C ∧ x ∈ A → ∃ x x = C ∧ x ∈ B
29 dfclel ⊢ C ∈ A ↔ ∃ x x = C ∧ x ∈ A
30 dfclel ⊢ C ∈ B ↔ ∃ x x = C ∧ x ∈ B
31 28 29 30 3imtr4g ⊢ A = B → C ∈ A → C ∈ B
32 4 5 8 15 31 wl-dfcleq.just ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B