Proof of Theorem eqoreldifOLD
Step | Hyp | Ref
| Expression |
1 | | orc 400 |
. . . . 5
⊢ (𝐴 = 𝐵 → (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵}))) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝐴 = 𝐵 → ((𝐵 ∈ 𝐶 ∧ 𝐴 ∈ 𝐶) → (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵})))) |
3 | | simprr 796 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐵 ∈ 𝐶 ∧ 𝐴 ∈ 𝐶)) → 𝐴 ∈ 𝐶) |
4 | | elsni 4194 |
. . . . . . . . . 10
⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) |
5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝐶 ∧ 𝐴 ∈ 𝐶) → (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)) |
6 | 5 | con3d 148 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝐶 ∧ 𝐴 ∈ 𝐶) → (¬ 𝐴 = 𝐵 → ¬ 𝐴 ∈ {𝐵})) |
7 | 6 | impcom 446 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐵 ∈ 𝐶 ∧ 𝐴 ∈ 𝐶)) → ¬ 𝐴 ∈ {𝐵}) |
8 | 3, 7 | eldifd 3585 |
. . . . . 6
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐵 ∈ 𝐶 ∧ 𝐴 ∈ 𝐶)) → 𝐴 ∈ (𝐶 ∖ {𝐵})) |
9 | 8 | olcd 408 |
. . . . 5
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐵 ∈ 𝐶 ∧ 𝐴 ∈ 𝐶)) → (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵}))) |
10 | 9 | ex 450 |
. . . 4
⊢ (¬
𝐴 = 𝐵 → ((𝐵 ∈ 𝐶 ∧ 𝐴 ∈ 𝐶) → (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵})))) |
11 | 2, 10 | pm2.61i 176 |
. . 3
⊢ ((𝐵 ∈ 𝐶 ∧ 𝐴 ∈ 𝐶) → (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵}))) |
12 | 11 | ex 450 |
. 2
⊢ (𝐵 ∈ 𝐶 → (𝐴 ∈ 𝐶 → (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵})))) |
13 | | eleq1 2689 |
. . . . 5
⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) |
14 | 13 | biimprd 238 |
. . . 4
⊢ (𝐴 = 𝐵 → (𝐵 ∈ 𝐶 → 𝐴 ∈ 𝐶)) |
15 | | eldifi 3732 |
. . . . 5
⊢ (𝐴 ∈ (𝐶 ∖ {𝐵}) → 𝐴 ∈ 𝐶) |
16 | 15 | a1d 25 |
. . . 4
⊢ (𝐴 ∈ (𝐶 ∖ {𝐵}) → (𝐵 ∈ 𝐶 → 𝐴 ∈ 𝐶)) |
17 | 14, 16 | jaoi 394 |
. . 3
⊢ ((𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵})) → (𝐵 ∈ 𝐶 → 𝐴 ∈ 𝐶)) |
18 | 17 | com12 32 |
. 2
⊢ (𝐵 ∈ 𝐶 → ((𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵})) → 𝐴 ∈ 𝐶)) |
19 | 12, 18 | impbid 202 |
1
⊢ (𝐵 ∈ 𝐶 → (𝐴 ∈ 𝐶 ↔ (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵})))) |