Step | Hyp | Ref
| Expression |
1 | | biass 374 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))) |
2 | 1 | notbii 310 |
. . . . . 6
⊢ (¬
((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ↔ ¬ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))) |
3 | | xor3 372 |
. . . . . . . 8
⊢ (¬
(¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ↔ (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ 𝐶)) |
4 | | notbi 309 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ↔ (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ 𝐶)) |
5 | 3, 4 | bitr4i 267 |
. . . . . . 7
⊢ (¬
(¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)) |
6 | 5 | con1bii 346 |
. . . . . 6
⊢ (¬
((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶) ↔ (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)) |
7 | | xor3 372 |
. . . . . 6
⊢ (¬
(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ↔ ¬ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))) |
8 | 2, 6, 7 | 3bitr3ri 291 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↔ ¬ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) ↔ (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)) |
9 | | elsymdif 3849 |
. . . . . 6
⊢ (𝑥 ∈ (𝐵 △ 𝐶) ↔ ¬ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)) |
10 | 9 | bibi2i 327 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐵 △ 𝐶)) ↔ (𝑥 ∈ 𝐴 ↔ ¬ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))) |
11 | | elsymdif 3849 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 △ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
12 | 11 | bibi1i 328 |
. . . . 5
⊢ ((𝑥 ∈ (𝐴 △ 𝐵) ↔ 𝑥 ∈ 𝐶) ↔ (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐶)) |
13 | 8, 10, 12 | 3bitr4i 292 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐵 △ 𝐶)) ↔ (𝑥 ∈ (𝐴 △ 𝐵) ↔ 𝑥 ∈ 𝐶)) |
14 | 13 | notbii 310 |
. . 3
⊢ (¬
(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐵 △ 𝐶)) ↔ ¬ (𝑥 ∈ (𝐴 △ 𝐵) ↔ 𝑥 ∈ 𝐶)) |
15 | | elsymdif 3849 |
. . 3
⊢ (𝑥 ∈ (𝐴 △ (𝐵 △ 𝐶)) ↔ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐵 △ 𝐶))) |
16 | | elsymdif 3849 |
. . 3
⊢ (𝑥 ∈ ((𝐴 △ 𝐵) △ 𝐶) ↔ ¬ (𝑥 ∈ (𝐴 △ 𝐵) ↔ 𝑥 ∈ 𝐶)) |
17 | 14, 15, 16 | 3bitr4i 292 |
. 2
⊢ (𝑥 ∈ (𝐴 △ (𝐵 △ 𝐶)) ↔ 𝑥 ∈ ((𝐴 △ 𝐵) △ 𝐶)) |
18 | 17 | eqriv 2619 |
1
⊢ (𝐴 △ (𝐵 △ 𝐶)) = ((𝐴 △ 𝐵) △ 𝐶) |