| Step | Hyp | Ref
| Expression |
| 1 | | nfra1 3284 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 |
| 2 | | rspa 3248 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
| 3 | | clel3g 3661 |
. . . . . . 7
⊢ (𝐵 ∈ 𝐶 → (𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))) |
| 4 | 2, 3 | syl 17 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))) |
| 5 | 1, 4 | rexbida 3272 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))) |
| 6 | | rexcom4 3288 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)) |
| 7 | 5, 6 | bitrdi 287 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))) |
| 8 | | r19.41v 3189 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)) |
| 9 | 8 | exbii 1848 |
. . . . 5
⊢
(∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)) |
| 10 | | exancom 1861 |
. . . . 5
⊢
(∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
| 11 | 9, 10 | bitri 275 |
. . . 4
⊢
(∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
| 12 | 7, 11 | bitrdi 287 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵))) |
| 13 | | eliun 4995 |
. . 3
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) |
| 14 | | eluniab 4921 |
. . 3
⊢ (𝑧 ∈ ∪ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = 𝐵} ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
| 15 | 12, 13, 14 | 3bitr4g 314 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ 𝑧 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})) |
| 16 | 15 | eqrdv 2735 |
1
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |