Step | Hyp | Ref
| Expression |
1 | | df-rex 2454 |
. . . . . . 7
⊢
(∃𝑧 ∈
𝐵 𝑦 ∈ 𝑧 ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
2 | 1 | rexbii 2477 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑧 ∈ 𝐵 𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝐴 ∃𝑧(𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
3 | | rexcom4 2753 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑧(𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧) ↔ ∃𝑧∃𝑥 ∈ 𝐴 (𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
4 | 2, 3 | bitri 183 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∃𝑧 ∈ 𝐵 𝑦 ∈ 𝑧 ↔ ∃𝑧∃𝑥 ∈ 𝐴 (𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
5 | | r19.41v 2626 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 (𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
6 | 5 | exbii 1598 |
. . . . 5
⊢
(∃𝑧∃𝑥 ∈ 𝐴 (𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧) ↔ ∃𝑧(∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
7 | 4, 6 | bitri 183 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 ∃𝑧 ∈ 𝐵 𝑦 ∈ 𝑧 ↔ ∃𝑧(∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
8 | | eluni2 3798 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝐵
↔ ∃𝑧 ∈
𝐵 𝑦 ∈ 𝑧) |
9 | 8 | rexbii 2477 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑦 ∈ 𝑧) |
10 | | df-rex 2454 |
. . . . 5
⊢
(∃𝑧 ∈
∪ 𝑥 ∈ 𝐴 𝐵𝑦 ∈ 𝑧 ↔ ∃𝑧(𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ 𝑧)) |
11 | | eliun 3875 |
. . . . . . 7
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) |
12 | 11 | anbi1i 455 |
. . . . . 6
⊢ ((𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
13 | 12 | exbii 1598 |
. . . . 5
⊢
(∃𝑧(𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ 𝑧) ↔ ∃𝑧(∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
14 | 10, 13 | bitri 183 |
. . . 4
⊢
(∃𝑧 ∈
∪ 𝑥 ∈ 𝐴 𝐵𝑦 ∈ 𝑧 ↔ ∃𝑧(∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝑧)) |
15 | 7, 9, 14 | 3bitr4i 211 |
. . 3
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ ∪ 𝐵 ↔ ∃𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑦 ∈ 𝑧) |
16 | | eliun 3875 |
. . 3
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ∪ 𝐵) |
17 | | eluni2 3798 |
. . 3
⊢ (𝑦 ∈ ∪ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑦 ∈ 𝑧) |
18 | 15, 16, 17 | 3bitr4i 211 |
. 2
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 ↔ 𝑦 ∈ ∪ ∪ 𝑥 ∈ 𝐴 𝐵) |
19 | 18 | eqriv 2167 |
1
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪
∪ 𝑥 ∈ 𝐴 𝐵 |