Step | Hyp | Ref
| Expression |
1 | | 19.43 1516 |
. . . 4
⊢ (∃y((x ∈ y ∧ y ∈ A) ∨ (x ∈ y ∧ y ∈ B)) ↔ (∃y(x ∈ y ∧ y ∈ A) ∨ ∃y(x ∈ y ∧ y ∈ B))) |
2 | | elun 3078 |
. . . . . . 7
⊢ (y ∈ (A ∪ B)
↔ (y ∈ A ∨ y ∈ B)) |
3 | 2 | anbi2i 430 |
. . . . . 6
⊢
((x ∈ y ∧ y ∈ (A ∪
B)) ↔ (x ∈ y ∧ (y ∈ A ∨ y ∈ B))) |
4 | | andi 730 |
. . . . . 6
⊢
((x ∈ y ∧ (y ∈ A ∨ y ∈ B)) ↔
((x ∈
y ∧
y ∈
A) ∨
(x ∈
y ∧
y ∈
B))) |
5 | 3, 4 | bitri 173 |
. . . . 5
⊢
((x ∈ y ∧ y ∈ (A ∪
B)) ↔ ((x ∈ y ∧ y ∈ A) ∨ (x ∈ y ∧ y ∈ B))) |
6 | 5 | exbii 1493 |
. . . 4
⊢ (∃y(x ∈ y ∧ y ∈ (A ∪ B))
↔ ∃y((x ∈ y ∧ y ∈ A) ∨ (x ∈ y ∧ y ∈ B))) |
7 | | eluni 3574 |
. . . . 5
⊢ (x ∈ ∪ A ↔ ∃y(x ∈ y ∧ y ∈ A)) |
8 | | eluni 3574 |
. . . . 5
⊢ (x ∈ ∪ B ↔ ∃y(x ∈ y ∧ y ∈ B)) |
9 | 7, 8 | orbi12i 680 |
. . . 4
⊢
((x ∈ ∪ A ∨ x ∈ ∪ B) ↔ (∃y(x ∈ y ∧ y ∈ A) ∨ ∃y(x ∈ y ∧ y ∈ B))) |
10 | 1, 6, 9 | 3bitr4i 201 |
. . 3
⊢ (∃y(x ∈ y ∧ y ∈ (A ∪ B))
↔ (x ∈ ∪ A ∨ x ∈ ∪ B)) |
11 | | eluni 3574 |
. . 3
⊢ (x ∈ ∪ (A ∪ B) ↔ ∃y(x ∈ y ∧ y ∈ (A ∪ B))) |
12 | | elun 3078 |
. . 3
⊢ (x ∈ (∪ A ∪ ∪ B) ↔ (x ∈ ∪ A ∨ x ∈ ∪ B)) |
13 | 10, 11, 12 | 3bitr4i 201 |
. 2
⊢ (x ∈ ∪ (A ∪ B) ↔ x
∈ (∪ A ∪ ∪ B)) |
14 | 13 | eqriv 2034 |
1
⊢ ∪ (A ∪ B) = (∪ A ∪ ∪ B) |