Step | Hyp | Ref
| Expression |
1 | | relxp 5656 |
. . . . . . . 8
⊢ Rel
(𝐴 × {𝑦}) |
2 | 1 | rgenw 3069 |
. . . . . . 7
⊢
∀𝑦 ∈
𝐵 Rel (𝐴 × {𝑦}) |
3 | | reliun 5777 |
. . . . . . 7
⊢ (Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∀𝑦 ∈ 𝐵 Rel (𝐴 × {𝑦})) |
4 | 2, 3 | mpbir 230 |
. . . . . 6
⊢ Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) |
5 | | elrel 5759 |
. . . . . 6
⊢ ((Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) → ∃𝑥∃𝑦 𝐶 = ⟨𝑥, 𝑦⟩) |
6 | 4, 5 | mpan 689 |
. . . . 5
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) → ∃𝑥∃𝑦 𝐶 = ⟨𝑥, 𝑦⟩) |
7 | | excom 2163 |
. . . . 5
⊢
(∃𝑦∃𝑥 𝐶 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦 𝐶 = ⟨𝑥, 𝑦⟩) |
8 | 6, 7 | sylibr 233 |
. . . 4
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) → ∃𝑦∃𝑥 𝐶 = ⟨𝑥, 𝑦⟩) |
9 | 8 | pm4.71ri 562 |
. . 3
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (∃𝑦∃𝑥 𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
10 | | nfiu1 4993 |
. . . . 5
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) |
11 | 10 | nfel2 2926 |
. . . 4
⊢
Ⅎ𝑦 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) |
12 | 11 | 19.41 2229 |
. . 3
⊢
(∃𝑦(∃𝑥 𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (∃𝑦∃𝑥 𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
13 | | 19.41v 1954 |
. . . . 5
⊢
(∃𝑥(𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (∃𝑥 𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
14 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝐶 = ⟨𝑥, 𝑦⟩ → (𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
15 | | opeliun2xp 46482 |
. . . . . . . . 9
⊢
(⟨𝑥, 𝑦⟩ ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) |
16 | 15 | biancomi 464 |
. . . . . . . 8
⊢
(⟨𝑥, 𝑦⟩ ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
17 | 14, 16 | bitrdi 287 |
. . . . . . 7
⊢ (𝐶 = ⟨𝑥, 𝑦⟩ → (𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
18 | 17 | pm5.32i 576 |
. . . . . 6
⊢ ((𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
19 | 18 | exbii 1851 |
. . . . 5
⊢
(∃𝑥(𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑥(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
20 | 13, 19 | bitr3i 277 |
. . . 4
⊢
((∃𝑥 𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑥(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
21 | 20 | exbii 1851 |
. . 3
⊢
(∃𝑦(∃𝑥 𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑦∃𝑥(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
22 | 9, 12, 21 | 3bitr2i 299 |
. 2
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑦∃𝑥(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
23 | | excom 2163 |
. 2
⊢
(∃𝑦∃𝑥(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ↔ ∃𝑥∃𝑦(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
24 | 22, 23 | bitri 275 |
1
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |