Step | Hyp | Ref
| Expression |
1 | | iuneqconst.p |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) |
2 | 1 | eleq2d 2897 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)) |
3 | 2 | rspcev 3620 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
4 | 3 | adantlr 713 |
. . . . 5
⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) ∧ 𝑦 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
5 | 4 | ex 415 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑦 ∈ 𝐶 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
6 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑥 𝑋 ∈ 𝐴 |
7 | | nfra1 3218 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 = 𝐶 |
8 | 6, 7 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑥(𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) |
9 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑥 𝑦 ∈ 𝐶 |
10 | | rsp 3204 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)) |
11 | | eleq2 2900 |
. . . . . . . 8
⊢ (𝐵 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)) |
12 | 11 | biimpd 231 |
. . . . . . 7
⊢ (𝐵 = 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
13 | 10, 12 | syl6 35 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝐵 = 𝐶 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))) |
14 | 13 | adantl 484 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))) |
15 | 8, 9, 14 | rexlimd 3316 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
16 | 5, 15 | impbid 214 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
17 | | eliun 4916 |
. . 3
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
18 | 16, 17 | syl6rbbr 292 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ 𝐶)) |
19 | 18 | eqrdv 2818 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → ∪
𝑥 ∈ 𝐴 𝐵 = 𝐶) |