Proof of Theorem rexiunxp
Step | Hyp | Ref
| Expression |
1 | | eliunxp 4748 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵))) |
2 | 1 | anbi1i 455 |
. . . . 5
⊢ ((𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) ∧ 𝜑) ↔ (∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑)) |
3 | | 19.41vv 1896 |
. . . . 5
⊢
(∃𝑦∃𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑) ↔ (∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑)) |
4 | 2, 3 | bitr4i 186 |
. . . 4
⊢ ((𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) ∧ 𝜑) ↔ ∃𝑦∃𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑)) |
5 | 4 | exbii 1598 |
. . 3
⊢
(∃𝑥(𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑)) |
6 | | exrot3 1683 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑) ↔ ∃𝑦∃𝑧∃𝑥((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑)) |
7 | | anass 399 |
. . . . . . 7
⊢ (((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑) ↔ (𝑥 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜑))) |
8 | 7 | exbii 1598 |
. . . . . 6
⊢
(∃𝑥((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑) ↔ ∃𝑥(𝑥 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜑))) |
9 | | vex 2733 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
10 | | vex 2733 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
11 | 9, 10 | opex 4212 |
. . . . . . 7
⊢
〈𝑦, 𝑧〉 ∈ V |
12 | | ralxp.1 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) |
13 | 12 | anbi2d 461 |
. . . . . . 7
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜑) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜓))) |
14 | 11, 13 | ceqsexv 2769 |
. . . . . 6
⊢
(∃𝑥(𝑥 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜑)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜓)) |
15 | 8, 14 | bitri 183 |
. . . . 5
⊢
(∃𝑥((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜓)) |
16 | 15 | 2exbii 1599 |
. . . 4
⊢
(∃𝑦∃𝑧∃𝑥((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑) ↔ ∃𝑦∃𝑧((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜓)) |
17 | 6, 16 | bitri 183 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝜑) ↔ ∃𝑦∃𝑧((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜓)) |
18 | 5, 17 | bitri 183 |
. 2
⊢
(∃𝑥(𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) ∧ 𝜑) ↔ ∃𝑦∃𝑧((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜓)) |
19 | | df-rex 2454 |
. 2
⊢
(∃𝑥 ∈
∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑥(𝑥 ∈ ∪
𝑦 ∈ 𝐴 ({𝑦} × 𝐵) ∧ 𝜑)) |
20 | | r2ex 2490 |
. 2
⊢
(∃𝑦 ∈
𝐴 ∃𝑧 ∈ 𝐵 𝜓 ↔ ∃𝑦∃𝑧((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ∧ 𝜓)) |
21 | 18, 19, 20 | 3bitr4i 211 |
1
⊢
(∃𝑥 ∈
∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) |