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 | ⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1w | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) ) | |
| 2 | eleq1w | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) ) | |
| 3 | 1 2 | bibi12d | ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) ) ) |
| 4 | 3 | cbvalvw | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) ) |
| 5 | eqid | ⊢ 𝐴 = 𝐴 | |
| 6 | eqtr | ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐶 ) | |
| 7 | 6 | eqcomd | ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐶 = 𝐴 ) |
| 8 | 7 | ex | ⊢ ( 𝐴 = 𝐵 → ( 𝐵 = 𝐶 → 𝐶 = 𝐴 ) ) |
| 9 | eqeq2 | ⊢ ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 ↔ 𝑥 = 𝐵 ) ) | |
| 10 | 9 | biimpd | ⊢ ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 → 𝑥 = 𝐵 ) ) |
| 11 | 10 | anim1d | ⊢ ( 𝐴 = 𝐵 → ( ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) ) |
| 12 | 11 | eximdv | ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) ) |
| 13 | dfclel | ⊢ ( 𝐴 ∈ 𝐶 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶 ) ) | |
| 14 | dfclel | ⊢ ( 𝐵 ∈ 𝐶 ↔ ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) | |
| 15 | 12 13 14 | 3imtr4g | ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝐶 → 𝐵 ∈ 𝐶 ) ) |
| 16 | wl-dfcleq.basic | ⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) ) | |
| 17 | biimp | ⊢ ( ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) ) | |
| 18 | 17 | alimi | ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) → ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) ) |
| 19 | 1 | biimpd | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ) |
| 20 | 19 | eqcoms | ⊢ ( 𝑦 = 𝑥 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ) |
| 21 | eleq1w | ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) ) | |
| 22 | 21 | biimpd | ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝐵 ) ) |
| 23 | 20 22 | imim12d | ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) ) |
| 24 | 23 | spimvw | ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) |
| 25 | 18 24 | syl | ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) |
| 26 | 16 25 | sylbi | ⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) |
| 27 | 26 | anim2d | ⊢ ( 𝐴 = 𝐵 → ( ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) ) |
| 28 | 27 | eximdv | ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) ) |
| 29 | dfclel | ⊢ ( 𝐶 ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) ) | |
| 30 | dfclel | ⊢ ( 𝐶 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) | |
| 31 | 28 29 30 | 3imtr4g | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) ) |
| 32 | 4 5 8 15 31 | wl-dfcleq.just | ⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) |