Step | Hyp | Ref
| Expression |
1 | | eliun 4928 |
. . 3
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
2 | | iuneqconst.p |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) |
3 | 2 | eleq2d 2824 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)) |
4 | 3 | rspcev 3561 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
5 | 4 | adantlr 712 |
. . . . 5
⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) ∧ 𝑦 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
6 | 5 | ex 413 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑦 ∈ 𝐶 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
7 | | nfv 1917 |
. . . . . 6
⊢
Ⅎ𝑥 𝑋 ∈ 𝐴 |
8 | | nfra1 3144 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 = 𝐶 |
9 | 7, 8 | nfan 1902 |
. . . . 5
⊢
Ⅎ𝑥(𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) |
10 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑥 𝑦 ∈ 𝐶 |
11 | | rsp 3131 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)) |
12 | | eleq2 2827 |
. . . . . . . 8
⊢ (𝐵 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)) |
13 | 12 | biimpd 228 |
. . . . . . 7
⊢ (𝐵 = 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
14 | 11, 13 | syl6 35 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))) |
15 | 14 | adantl 482 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))) |
16 | 9, 10, 15 | rexlimd 3250 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
17 | 6, 16 | impbid 211 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
18 | 1, 17 | bitr4id 290 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ 𝐶)) |
19 | 18 | eqrdv 2736 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → ∪
𝑥 ∈ 𝐴 𝐵 = 𝐶) |