| Step | Hyp | Ref
| Expression |
| 1 | | elxp 5708 |
. . 3
⊢ (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴))) |
| 2 | | df-rex 3071 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
| 3 | | an13 647 |
. . . . . . 7
⊢ ((𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) ↔ (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
| 4 | 3 | exbii 1848 |
. . . . . 6
⊢
(∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
| 5 | 2, 4 | bitr4i 278 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ ∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴))) |
| 6 | | elsni 4643 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑋} → 𝑥 = 𝑋) |
| 7 | 6 | opeq1d 4879 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑋} → 〈𝑥, 𝑦〉 = 〈𝑋, 𝑦〉) |
| 8 | 7 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑋} → (𝑍 = 〈𝑥, 𝑦〉 ↔ 𝑍 = 〈𝑋, 𝑦〉)) |
| 9 | 8 | biimpa 476 |
. . . . . 6
⊢ ((𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) → 𝑍 = 〈𝑋, 𝑦〉) |
| 10 | 9 | reximi 3084 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
| 11 | 5, 10 | sylbir 235 |
. . . 4
⊢
(∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
| 12 | 11 | exlimiv 1930 |
. . 3
⊢
(∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
| 13 | 1, 12 | sylbi 217 |
. 2
⊢ (𝑍 ∈ ({𝑋} × 𝐴) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
| 14 | | snidg 4660 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
| 15 | | opelxpi 5722 |
. . . . 5
⊢ ((𝑋 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
| 16 | 14, 15 | sylan 580 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
| 17 | | eleq1 2829 |
. . . 4
⊢ (𝑍 = 〈𝑋, 𝑦〉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴))) |
| 18 | 16, 17 | syl5ibrcom 247 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑍 = 〈𝑋, 𝑦〉 → 𝑍 ∈ ({𝑋} × 𝐴))) |
| 19 | 18 | rexlimdva 3155 |
. 2
⊢ (𝑋 ∈ 𝑉 → (∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉 → 𝑍 ∈ ({𝑋} × 𝐴))) |
| 20 | 13, 19 | impbid2 226 |
1
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉)) |