Proof of Theorem eliunxp
Step | Hyp | Ref
| Expression |
1 | | relxp 4390 |
. . . . . 6
⊢ Rel
({x} × B) |
2 | 1 | rgenw 2370 |
. . . . 5
⊢ ∀x ∈ A Rel
({x} × B) |
3 | | reliun 4401 |
. . . . 5
⊢ (Rel
∪ x ∈ A ({x} × B)
↔ ∀x ∈ A Rel ({x}
× B)) |
4 | 2, 3 | mpbir 134 |
. . . 4
⊢ Rel
∪ x ∈ A ({x} × B) |
5 | | elrel 4385 |
. . . 4
⊢ ((Rel
∪ x ∈ A ({x} × B)
∧ 𝐶 ∈
∪ x ∈ A ({x} × B))
→ ∃x∃y 𝐶 = 〈x, y〉) |
6 | 4, 5 | mpan 400 |
. . 3
⊢ (𝐶 ∈ ∪ x ∈ A ({x} ×
B) → ∃x∃y 𝐶 = 〈x, y〉) |
7 | 6 | pm4.71ri 372 |
. 2
⊢ (𝐶 ∈ ∪ x ∈ A ({x} ×
B) ↔ (∃x∃y 𝐶 = 〈x, y〉 ∧ 𝐶 ∈
∪ x ∈ A ({x} × B))) |
8 | | nfiu1 3678 |
. . . 4
⊢
Ⅎx∪ x ∈ A ({x} × B) |
9 | 8 | nfel2 2187 |
. . 3
⊢
Ⅎx 𝐶 ∈
∪ x ∈ A ({x} × B) |
10 | 9 | 19.41 1573 |
. 2
⊢ (∃x(∃y 𝐶 = 〈x, y〉 ∧ 𝐶 ∈
∪ x ∈ A ({x} × B))
↔ (∃x∃y 𝐶 = 〈x, y〉 ∧ 𝐶 ∈
∪ x ∈ A ({x} × B))) |
11 | | 19.41v 1779 |
. . . 4
⊢ (∃y(𝐶 = 〈x, y〉 ∧ 𝐶 ∈
∪ x ∈ A ({x} × B))
↔ (∃y 𝐶 = 〈x, y〉 ∧ 𝐶 ∈
∪ x ∈ A ({x} × B))) |
12 | | eleq1 2097 |
. . . . . . 7
⊢ (𝐶 = 〈x, y〉
→ (𝐶 ∈ ∪ x ∈ A ({x} ×
B) ↔ 〈x, y〉 ∈ ∪ x ∈ A ({x} ×
B))) |
13 | | opeliunxp 4338 |
. . . . . . 7
⊢
(〈x, y〉 ∈ ∪ x ∈ A ({x} × B)
↔ (x ∈ A ∧ y ∈ B)) |
14 | 12, 13 | syl6bb 185 |
. . . . . 6
⊢ (𝐶 = 〈x, y〉
→ (𝐶 ∈ ∪ x ∈ A ({x} ×
B) ↔ (x ∈ A ∧ y ∈ B))) |
15 | 14 | pm5.32i 427 |
. . . . 5
⊢ ((𝐶 = 〈x, y〉 ∧ 𝐶 ∈
∪ x ∈ A ({x} × B))
↔ (𝐶 = 〈x, y〉 ∧ (x ∈ A ∧ y ∈ B))) |
16 | 15 | exbii 1493 |
. . . 4
⊢ (∃y(𝐶 = 〈x, y〉 ∧ 𝐶 ∈
∪ x ∈ A ({x} × B))
↔ ∃y(𝐶 = 〈x, y〉 ∧ (x ∈ A ∧ y ∈ B))) |
17 | 11, 16 | bitr3i 175 |
. . 3
⊢ ((∃y 𝐶 = 〈x, y〉 ∧ 𝐶 ∈
∪ x ∈ A ({x} × B))
↔ ∃y(𝐶 = 〈x, y〉 ∧ (x ∈ A ∧ y ∈ B))) |
18 | 17 | exbii 1493 |
. 2
⊢ (∃x(∃y 𝐶 = 〈x, y〉 ∧ 𝐶 ∈
∪ x ∈ A ({x} × B))
↔ ∃x∃y(𝐶 = 〈x, y〉 ∧ (x ∈ A ∧ y ∈ B))) |
19 | 7, 10, 18 | 3bitr2i 197 |
1
⊢ (𝐶 ∈ ∪ x ∈ A ({x} ×
B) ↔ ∃x∃y(𝐶 = 〈x, y〉 ∧ (x ∈ A ∧ y ∈ B))) |