Proof of Theorem raliunxp
Step | Hyp | Ref
| Expression |
1 | | eliunxp 4750 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵))) |
2 | 1 | imbi1i 237 |
. . . . 5
⊢ ((𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) → 𝜑) ↔ (∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑)) |
3 | | 19.23vv 1877 |
. . . . 5
⊢
(∀𝑦∀𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑) ↔ (∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑)) |
4 | 2, 3 | bitr4i 186 |
. . . 4
⊢ ((𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) → 𝜑) ↔ ∀𝑦∀𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑)) |
5 | 4 | albii 1463 |
. . 3
⊢
(∀𝑥(𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) → 𝜑) ↔ ∀𝑥∀𝑦∀𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑)) |
6 | | alrot3 1478 |
. . . 4
⊢
(∀𝑥∀𝑦∀𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑) ↔ ∀𝑦∀𝑧∀𝑥((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑)) |
7 | | impexp 261 |
. . . . . . 7
⊢ (((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑) ↔ (𝑥 = 〈𝑦, 𝑧〉 → ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜑))) |
8 | 7 | albii 1463 |
. . . . . 6
⊢
(∀𝑥((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑) ↔ ∀𝑥(𝑥 = 〈𝑦, 𝑧〉 → ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜑))) |
9 | | vex 2733 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
10 | | vex 2733 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
11 | 9, 10 | opex 4214 |
. . . . . . 7
⊢
〈𝑦, 𝑧〉 ∈ V |
12 | | ralxp.1 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) |
13 | 12 | imbi2d 229 |
. . . . . . 7
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜑) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜓))) |
14 | 11, 13 | ceqsalv 2760 |
. . . . . 6
⊢
(∀𝑥(𝑥 = 〈𝑦, 𝑧〉 → ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜑)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜓)) |
15 | 8, 14 | bitri 183 |
. . . . 5
⊢
(∀𝑥((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜓)) |
16 | 15 | 2albii 1464 |
. . . 4
⊢
(∀𝑦∀𝑧∀𝑥((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑) ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜓)) |
17 | 6, 16 | bitri 183 |
. . 3
⊢
(∀𝑥∀𝑦∀𝑧((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝜑) ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜓)) |
18 | 5, 17 | bitri 183 |
. 2
⊢
(∀𝑥(𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) → 𝜑) ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜓)) |
19 | | df-ral 2453 |
. 2
⊢
(∀𝑥 ∈
∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ ∪
𝑦 ∈ 𝐴 ({𝑦} × 𝐵) → 𝜑)) |
20 | | r2al 2489 |
. 2
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐵 𝜓 ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝜓)) |
21 | 18, 19, 20 | 3bitr4i 211 |
1
⊢
(∀𝑥 ∈
∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |