Step | Hyp | Ref
| Expression |
1 | | nfra1 2349 |
. . . . . 6
⊢
Ⅎx∀x ∈ A B ∈ 𝐶 |
2 | | rsp 2363 |
. . . . . . . 8
⊢ (∀x ∈ A B ∈ 𝐶 → (x ∈ A → B ∈ 𝐶)) |
3 | | clel3g 2672 |
. . . . . . . 8
⊢ (B ∈ 𝐶 → (z ∈ B ↔ ∃y(y = B ∧ z ∈ y))) |
4 | 2, 3 | syl6 29 |
. . . . . . 7
⊢ (∀x ∈ A B ∈ 𝐶 → (x ∈ A → (z
∈ B
↔ ∃y(y = B ∧ z ∈ y)))) |
5 | 4 | imp 115 |
. . . . . 6
⊢ ((∀x ∈ A B ∈ 𝐶 ∧ x ∈ A) →
(z ∈
B ↔ ∃y(y = B ∧ z ∈ y))) |
6 | 1, 5 | rexbida 2315 |
. . . . 5
⊢ (∀x ∈ A B ∈ 𝐶 → (∃x ∈ A z ∈ B ↔ ∃x ∈ A ∃y(y = B ∧ z ∈ y))) |
7 | | rexcom4 2571 |
. . . . 5
⊢ (∃x ∈ A ∃y(y = B ∧ z ∈ y) ↔
∃y∃x ∈ A (y = B ∧ z ∈ y)) |
8 | 6, 7 | syl6bb 185 |
. . . 4
⊢ (∀x ∈ A B ∈ 𝐶 → (∃x ∈ A z ∈ B ↔ ∃y∃x ∈ A (y = B ∧ z ∈ y))) |
9 | | r19.41v 2460 |
. . . . . 6
⊢ (∃x ∈ A (y = B ∧ z ∈ y) ↔
(∃x
∈ A
y = B
∧ z ∈ y)) |
10 | 9 | exbii 1493 |
. . . . 5
⊢ (∃y∃x ∈ A (y = B ∧ z ∈ y) ↔
∃y(∃x ∈ A y = B ∧ z ∈ y)) |
11 | | exancom 1496 |
. . . . 5
⊢ (∃y(∃x ∈ A y = B ∧ z ∈ y) ↔
∃y(z ∈ y ∧ ∃x ∈ A y = B)) |
12 | 10, 11 | bitri 173 |
. . . 4
⊢ (∃y∃x ∈ A (y = B ∧ z ∈ y) ↔
∃y(z ∈ y ∧ ∃x ∈ A y = B)) |
13 | 8, 12 | syl6bb 185 |
. . 3
⊢ (∀x ∈ A B ∈ 𝐶 → (∃x ∈ A z ∈ B ↔ ∃y(z ∈ y ∧ ∃x ∈ A y = B))) |
14 | | eliun 3652 |
. . 3
⊢ (z ∈ ∪ x ∈ A B ↔ ∃x ∈ A z ∈ B) |
15 | | eluniab 3583 |
. . 3
⊢ (z ∈ ∪ {y ∣ ∃x ∈ A y = B} ↔
∃y(z ∈ y ∧ ∃x ∈ A y = B)) |
16 | 13, 14, 15 | 3bitr4g 212 |
. 2
⊢ (∀x ∈ A B ∈ 𝐶 → (z ∈ ∪ x ∈ A B ↔ z ∈ ∪ {y ∣ ∃x ∈ A y = B})) |
17 | 16 | eqrdv 2035 |
1
⊢ (∀x ∈ A B ∈ 𝐶 → ∪ x ∈ A B = ∪ {y ∣ ∃x ∈ A y = B}) |