| Step | Hyp | Ref
| Expression |
| 1 | | df-rex 3071 |
. . 3
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜑)) |
| 2 | | 19.42v 1953 |
. . . . 5
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))) |
| 3 | | df-rex 3071 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐵 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑)) |
| 4 | 3 | anbi2i 623 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜑))) |
| 5 | 2, 4 | bitr4i 278 |
. . . 4
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜑)) |
| 6 | 5 | exbii 1848 |
. . 3
⊢
(∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜑)) |
| 7 | 1, 6 | bitr4i 278 |
. 2
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑))) |
| 8 | | rexunirn.2 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉) |
| 9 | | rexunirn.1 |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 10 | 9 | elrnmpt1 5971 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹) |
| 11 | 8, 10 | mpdan 687 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ ran 𝐹) |
| 12 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝐵)) |
| 13 | 12 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → ((𝑦 ∈ 𝑏 ∧ 𝜑) ↔ (𝑦 ∈ 𝐵 ∧ 𝜑))) |
| 14 | 13 | rspcev 3622 |
. . . . . . 7
⊢ ((𝐵 ∈ ran 𝐹 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) → ∃𝑏 ∈ ran 𝐹(𝑦 ∈ 𝑏 ∧ 𝜑)) |
| 15 | 11, 14 | sylan 580 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) → ∃𝑏 ∈ ran 𝐹(𝑦 ∈ 𝑏 ∧ 𝜑)) |
| 16 | | r19.41v 3189 |
. . . . . 6
⊢
(∃𝑏 ∈ ran
𝐹(𝑦 ∈ 𝑏 ∧ 𝜑) ↔ (∃𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑)) |
| 17 | 15, 16 | sylib 218 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) → (∃𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑)) |
| 18 | 17 | eximi 1835 |
. . . 4
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) → ∃𝑦(∃𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑)) |
| 19 | | df-rex 3071 |
. . . . 5
⊢
(∃𝑦 ∈
∪ ran 𝐹𝜑 ↔ ∃𝑦(𝑦 ∈ ∪ ran
𝐹 ∧ 𝜑)) |
| 20 | | eluni2 4911 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ ran 𝐹 ↔ ∃𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏) |
| 21 | 20 | anbi1i 624 |
. . . . . 6
⊢ ((𝑦 ∈ ∪ ran 𝐹 ∧ 𝜑) ↔ (∃𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑)) |
| 22 | 21 | exbii 1848 |
. . . . 5
⊢
(∃𝑦(𝑦 ∈ ∪ ran 𝐹 ∧ 𝜑) ↔ ∃𝑦(∃𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑)) |
| 23 | 19, 22 | bitri 275 |
. . . 4
⊢
(∃𝑦 ∈
∪ ran 𝐹𝜑 ↔ ∃𝑦(∃𝑏 ∈ ran 𝐹 𝑦 ∈ 𝑏 ∧ 𝜑)) |
| 24 | 18, 23 | sylibr 234 |
. . 3
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) → ∃𝑦 ∈ ∪ ran
𝐹𝜑) |
| 25 | 24 | exlimiv 1930 |
. 2
⊢
(∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 ∈ 𝐵 ∧ 𝜑)) → ∃𝑦 ∈ ∪ ran
𝐹𝜑) |
| 26 | 7, 25 | sylbi 217 |
1
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ ∪ ran
𝐹𝜑) |