| Step | Hyp | Ref
| Expression |
| 1 | | df-iun 4993 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} |
| 2 | | elisset 2823 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝐶 → ∃𝑧 𝑧 = 𝐵) |
| 3 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵)) |
| 4 | 3 | pm5.32ri 575 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐵 ∧ 𝑧 = 𝐵)) |
| 5 | 4 | simplbi2 500 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝐵 → (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))) |
| 6 | 5 | eximdv 1917 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐵 → (∃𝑧 𝑧 = 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))) |
| 7 | 2, 6 | syl5com 31 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝐶 → (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))) |
| 8 | 7 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → ∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))) |
| 9 | | rexim 3087 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)) → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))) |
| 10 | 8, 9 | syl 17 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))) |
| 11 | | rexcom4 3288 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)) |
| 12 | | r19.42v 3191 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
| 13 | 12 | exbii 1848 |
. . . . . . 7
⊢
(∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
| 14 | 11, 13 | bitri 275 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
| 15 | 10, 14 | imbitrdi 251 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))) |
| 16 | 3 | biimpac 478 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → 𝑤 ∈ 𝐵) |
| 17 | 16 | reximi 3084 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵) |
| 18 | 12, 17 | sylbir 235 |
. . . . . 6
⊢ ((𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵) |
| 19 | 18 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵) |
| 20 | 15, 19 | impbid1 225 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))) |
| 21 | | vex 3484 |
. . . . 5
⊢ 𝑤 ∈ V |
| 22 | | eleq1w 2824 |
. . . . . 6
⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵)) |
| 23 | 22 | rexbidv 3179 |
. . . . 5
⊢ (𝑧 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)) |
| 24 | 21, 23 | elab 3679 |
. . . 4
⊢ (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵) |
| 25 | | eluni 4910 |
. . . . 5
⊢ (𝑤 ∈ ∪ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})) |
| 26 | | vex 3484 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
| 27 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑧 = 𝐵)) |
| 28 | 27 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
| 29 | 26, 28 | elab 3679 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
| 30 | 29 | anbi2i 623 |
. . . . . 6
⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
| 31 | 30 | exbii 1848 |
. . . . 5
⊢
(∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
| 32 | 25, 31 | bitri 275 |
. . . 4
⊢ (𝑤 ∈ ∪ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
| 33 | 20, 24, 32 | 3bitr4g 314 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ 𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})) |
| 34 | 33 | eqrdv 2735 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
| 35 | 1, 34 | eqtrid 2789 |
1
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |