Step | Hyp | Ref
| Expression |
1 | | elxp 5574 |
. . 3
⊢ (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴))) |
2 | | df-rex 3067 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
3 | | an13 647 |
. . . . . . 7
⊢ ((𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) ↔ (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
4 | 3 | exbii 1855 |
. . . . . 6
⊢
(∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
5 | 2, 4 | bitr4i 281 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ ∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴))) |
6 | | elsni 4558 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑋} → 𝑥 = 𝑋) |
7 | 6 | opeq1d 4790 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑋} → 〈𝑥, 𝑦〉 = 〈𝑋, 𝑦〉) |
8 | 7 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑋} → (𝑍 = 〈𝑥, 𝑦〉 ↔ 𝑍 = 〈𝑋, 𝑦〉)) |
9 | 8 | biimpa 480 |
. . . . . 6
⊢ ((𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) → 𝑍 = 〈𝑋, 𝑦〉) |
10 | 9 | reximi 3166 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
11 | 5, 10 | sylbir 238 |
. . . 4
⊢
(∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
12 | 11 | exlimiv 1938 |
. . 3
⊢
(∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
13 | 1, 12 | sylbi 220 |
. 2
⊢ (𝑍 ∈ ({𝑋} × 𝐴) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
14 | | snidg 4575 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
15 | | opelxpi 5588 |
. . . . 5
⊢ ((𝑋 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
16 | 14, 15 | sylan 583 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
17 | | eleq1 2825 |
. . . 4
⊢ (𝑍 = 〈𝑋, 𝑦〉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴))) |
18 | 16, 17 | syl5ibrcom 250 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑍 = 〈𝑋, 𝑦〉 → 𝑍 ∈ ({𝑋} × 𝐴))) |
19 | 18 | rexlimdva 3203 |
. 2
⊢ (𝑋 ∈ 𝑉 → (∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉 → 𝑍 ∈ ({𝑋} × 𝐴))) |
20 | 13, 19 | impbid2 229 |
1
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉)) |