Step | Hyp | Ref
| Expression |
1 | | df-rex 2306 |
. . . . . . 7
⊢ (∃z ∈ B y ∈ z ↔ ∃z(z ∈ B ∧ y ∈ z)) |
2 | 1 | rexbii 2325 |
. . . . . 6
⊢ (∃x ∈ A ∃z ∈ B y ∈ z ↔ ∃x ∈ A ∃z(z ∈ B ∧ y ∈ z)) |
3 | | rexcom4 2571 |
. . . . . 6
⊢ (∃x ∈ A ∃z(z ∈ B ∧ y ∈ z) ↔ ∃z∃x ∈ A (z ∈ B ∧ y ∈ z)) |
4 | 2, 3 | bitri 173 |
. . . . 5
⊢ (∃x ∈ A ∃z ∈ B y ∈ z ↔ ∃z∃x ∈ A (z ∈ B ∧ y ∈ z)) |
5 | | r19.41v 2460 |
. . . . . 6
⊢ (∃x ∈ A (z ∈ B ∧ y ∈ z) ↔ (∃x ∈ A z ∈ B ∧ y ∈ z)) |
6 | 5 | exbii 1493 |
. . . . 5
⊢ (∃z∃x ∈ A (z ∈ B ∧ y ∈ z) ↔ ∃z(∃x ∈ A z ∈ B ∧ y ∈ z)) |
7 | 4, 6 | bitri 173 |
. . . 4
⊢ (∃x ∈ A ∃z ∈ B y ∈ z ↔ ∃z(∃x ∈ A z ∈ B ∧ y ∈ z)) |
8 | | eluni2 3575 |
. . . . 5
⊢ (y ∈ ∪ B ↔ ∃z ∈ B y ∈ z) |
9 | 8 | rexbii 2325 |
. . . 4
⊢ (∃x ∈ A y ∈ ∪ B ↔ ∃x ∈ A ∃z ∈ B y ∈ z) |
10 | | df-rex 2306 |
. . . . 5
⊢ (∃z ∈ ∪ x ∈ A By ∈ z ↔ ∃z(z ∈ ∪ x ∈ A B ∧ y ∈ z)) |
11 | | eliun 3652 |
. . . . . . 7
⊢ (z ∈ ∪ x ∈ A B ↔ ∃x ∈ A z ∈ B) |
12 | 11 | anbi1i 431 |
. . . . . 6
⊢
((z ∈ ∪ x ∈ A B ∧ y ∈ z) ↔
(∃x
∈ A
z ∈
B ∧
y ∈
z)) |
13 | 12 | exbii 1493 |
. . . . 5
⊢ (∃z(z ∈ ∪ x ∈ A B ∧ y ∈ z) ↔ ∃z(∃x ∈ A z ∈ B ∧ y ∈ z)) |
14 | 10, 13 | bitri 173 |
. . . 4
⊢ (∃z ∈ ∪ x ∈ A By ∈ z ↔ ∃z(∃x ∈ A z ∈ B ∧ y ∈ z)) |
15 | 7, 9, 14 | 3bitr4i 201 |
. . 3
⊢ (∃x ∈ A y ∈ ∪ B ↔ ∃z ∈ ∪ x ∈ A By ∈ z) |
16 | | eliun 3652 |
. . 3
⊢ (y ∈ ∪ x ∈ A ∪ B ↔ ∃x ∈ A y ∈ ∪ B) |
17 | | eluni2 3575 |
. . 3
⊢ (y ∈ ∪ ∪ x ∈ A B ↔ ∃z ∈ ∪ x ∈ A By ∈ z) |
18 | 15, 16, 17 | 3bitr4i 201 |
. 2
⊢ (y ∈ ∪ x ∈ A ∪ B ↔ y ∈ ∪ ∪ x ∈ A B) |
19 | 18 | eqriv 2034 |
1
⊢ ∪ x ∈ A ∪ B = ∪ ∪ x ∈ A B |