Step | Hyp | Ref
| Expression |
1 | | elcnv2 5714 |
. . . 4
⊢ (𝑦 ∈ ◡∪ 𝐴 ↔ ∃𝑧∃𝑤(𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ ∪
𝐴)) |
2 | | eluni2 4797 |
. . . . . . 7
⊢
(〈𝑤, 𝑧〉 ∈ ∪ 𝐴
↔ ∃𝑥 ∈
𝐴 〈𝑤, 𝑧〉 ∈ 𝑥) |
3 | 2 | anbi2i 626 |
. . . . . 6
⊢ ((𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ ∪
𝐴) ↔ (𝑦 = 〈𝑧, 𝑤〉 ∧ ∃𝑥 ∈ 𝐴 〈𝑤, 𝑧〉 ∈ 𝑥)) |
4 | | r19.42v 3253 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 (𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥) ↔ (𝑦 = 〈𝑧, 𝑤〉 ∧ ∃𝑥 ∈ 𝐴 〈𝑤, 𝑧〉 ∈ 𝑥)) |
5 | 3, 4 | bitr4i 281 |
. . . . 5
⊢ ((𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ ∪
𝐴) ↔ ∃𝑥 ∈ 𝐴 (𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥)) |
6 | 5 | 2exbii 1855 |
. . . 4
⊢
(∃𝑧∃𝑤(𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ ∪
𝐴) ↔ ∃𝑧∃𝑤∃𝑥 ∈ 𝐴 (𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥)) |
7 | | elcnv2 5714 |
. . . . . 6
⊢ (𝑦 ∈ ◡𝑥 ↔ ∃𝑧∃𝑤(𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥)) |
8 | 7 | rexbii 3160 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 ∃𝑧∃𝑤(𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥)) |
9 | | rexcom4 3162 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∃𝑧∃𝑤(𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥) ↔ ∃𝑧∃𝑥 ∈ 𝐴 ∃𝑤(𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥)) |
10 | | rexcom4 3162 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑤(𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥) ↔ ∃𝑤∃𝑥 ∈ 𝐴 (𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥)) |
11 | 10 | exbii 1854 |
. . . . 5
⊢
(∃𝑧∃𝑥 ∈ 𝐴 ∃𝑤(𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥) ↔ ∃𝑧∃𝑤∃𝑥 ∈ 𝐴 (𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥)) |
12 | 8, 9, 11 | 3bitrri 301 |
. . . 4
⊢
(∃𝑧∃𝑤∃𝑥 ∈ 𝐴 (𝑦 = 〈𝑧, 𝑤〉 ∧ 〈𝑤, 𝑧〉 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ◡𝑥) |
13 | 1, 6, 12 | 3bitri 300 |
. . 3
⊢ (𝑦 ∈ ◡∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ◡𝑥) |
14 | | eliun 4882 |
. . 3
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ◡𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ◡𝑥) |
15 | 13, 14 | bitr4i 281 |
. 2
⊢ (𝑦 ∈ ◡∪ 𝐴 ↔ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 ◡𝑥) |
16 | 15 | eqriv 2735 |
1
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥 |