Step | Hyp | Ref
| Expression |
1 | | excom 1554 |
. . . . 5
⊢
(∃𝑧∃𝑥(〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥∃𝑧(〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) |
2 | | ancom 253 |
. . . . . . 7
⊢
((∃𝑧〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑧〈𝑦, 𝑧〉 ∈ 𝑥)) |
3 | | 19.41v 1782 |
. . . . . . 7
⊢
(∃𝑧(〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (∃𝑧〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) |
4 | | vex 2560 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
5 | 4 | eldm2 4533 |
. . . . . . . 8
⊢ (𝑦 ∈ dom 𝑥 ↔ ∃𝑧〈𝑦, 𝑧〉 ∈ 𝑥) |
6 | 5 | anbi2i 430 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑧〈𝑦, 𝑧〉 ∈ 𝑥)) |
7 | 2, 3, 6 | 3bitr4i 201 |
. . . . . 6
⊢
(∃𝑧(〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥)) |
8 | 7 | exbii 1496 |
. . . . 5
⊢
(∃𝑥∃𝑧(〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥)) |
9 | 1, 8 | bitri 173 |
. . . 4
⊢
(∃𝑧∃𝑥(〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥)) |
10 | | eluni 3583 |
. . . . 5
⊢
(〈𝑦, 𝑧〉 ∈ ∪ 𝐴
↔ ∃𝑥(〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) |
11 | 10 | exbii 1496 |
. . . 4
⊢
(∃𝑧〈𝑦, 𝑧〉 ∈ ∪
𝐴 ↔ ∃𝑧∃𝑥(〈𝑦, 𝑧〉 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) |
12 | | df-rex 2312 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ dom 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥)) |
13 | 9, 11, 12 | 3bitr4i 201 |
. . 3
⊢
(∃𝑧〈𝑦, 𝑧〉 ∈ ∪
𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥) |
14 | 4 | eldm2 4533 |
. . 3
⊢ (𝑦 ∈ dom ∪ 𝐴
↔ ∃𝑧〈𝑦, 𝑧〉 ∈ ∪
𝐴) |
15 | | eliun 3661 |
. . 3
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 dom 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥) |
16 | 13, 14, 15 | 3bitr4i 201 |
. 2
⊢ (𝑦 ∈ dom ∪ 𝐴
↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 dom 𝑥) |
17 | 16 | eqriv 2037 |
1
⊢ dom ∪ 𝐴 =
∪ 𝑥 ∈ 𝐴 dom 𝑥 |