Step | Hyp | Ref
| Expression |
1 | | 19.43 1605 |
. . . 4
⊢ (∃y((x ∈ y ∧ y ∈ A) ∨ (x ∈ y ∧ y ∈ B)) ↔ (∃y(x ∈ y ∧ y ∈ A) ∨ ∃y(x ∈ y ∧ y ∈ B))) |
2 | | elun 3220 |
. . . . . . 7
⊢ (y ∈ (A ∪ B)
↔ (y ∈ A ∨ y ∈ B)) |
3 | 2 | anbi2i 675 |
. . . . . 6
⊢ ((x ∈ y ∧ y ∈ (A ∪ B))
↔ (x ∈ y ∧ (y ∈ A ∨ y ∈ B))) |
4 | | andi 837 |
. . . . . 6
⊢ ((x ∈ y ∧ (y ∈ A ∨ y ∈ B)) ↔ ((x
∈ y ∧ y ∈ A) ∨ (x ∈ y ∧ y ∈ B))) |
5 | 3, 4 | bitri 240 |
. . . . 5
⊢ ((x ∈ y ∧ y ∈ (A ∪ B))
↔ ((x ∈ y ∧ y ∈ A) ∨ (x ∈ y ∧ y ∈ B))) |
6 | 5 | exbii 1582 |
. . . 4
⊢ (∃y(x ∈ y ∧ y ∈ (A ∪ B))
↔ ∃y((x ∈ y ∧ y ∈ A) ∨ (x ∈ y ∧ y ∈ B))) |
7 | | eluni 3894 |
. . . . 5
⊢ (x ∈ ∪A ↔ ∃y(x ∈ y ∧ y ∈ A)) |
8 | | eluni 3894 |
. . . . 5
⊢ (x ∈ ∪B ↔ ∃y(x ∈ y ∧ y ∈ B)) |
9 | 7, 8 | orbi12i 507 |
. . . 4
⊢ ((x ∈ ∪A ∨ x ∈ ∪B) ↔ (∃y(x ∈ y ∧ y ∈ A) ∨ ∃y(x ∈ y ∧ y ∈ B))) |
10 | 1, 6, 9 | 3bitr4i 268 |
. . 3
⊢ (∃y(x ∈ y ∧ y ∈ (A ∪ B))
↔ (x ∈ ∪A ∨ x ∈ ∪B)) |
11 | | eluni 3894 |
. . 3
⊢ (x ∈ ∪(A ∪ B) ↔ ∃y(x ∈ y ∧ y ∈ (A ∪ B))) |
12 | | elun 3220 |
. . 3
⊢ (x ∈ (∪A ∪ ∪B) ↔ (x ∈ ∪A ∨ x ∈ ∪B)) |
13 | 10, 11, 12 | 3bitr4i 268 |
. 2
⊢ (x ∈ ∪(A ∪ B) ↔ x
∈ (∪A ∪ ∪B)) |
14 | 13 | eqriv 2350 |
1
⊢ ∪(A ∪ B) = (∪A ∪ ∪B) |