Step | Hyp | Ref
| Expression |
1 | | ancom 460 |
. . . . 5
⊢ ((𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)) ↔ (∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥)) |
2 | | r19.41v 3184 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ (∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥)) |
3 | 1, 2 | bitr4i 278 |
. . . 4
⊢ ((𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)) ↔ ∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥)) |
4 | 3 | exbii 1843 |
. . 3
⊢
(∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)) ↔ ∃𝑥∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥)) |
5 | | eluniab 4917 |
. . 3
⊢ (𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 ∈
𝐴 𝑥 = (𝑦 ∩ 𝐵)} ↔ ∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵))) |
6 | | eluni2 4907 |
. . . . . 6
⊢ (𝑧 ∈ ∪ 𝐴
↔ ∃𝑦 ∈
𝐴 𝑧 ∈ 𝑦) |
7 | 6 | anbi1i 623 |
. . . . 5
⊢ ((𝑧 ∈ ∪ 𝐴
∧ 𝑧 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵)) |
8 | | elin 3961 |
. . . . 5
⊢ (𝑧 ∈ (∪ 𝐴
∩ 𝐵) ↔ (𝑧 ∈ ∪ 𝐴
∧ 𝑧 ∈ 𝐵)) |
9 | | r19.41v 3184 |
. . . . 5
⊢
(∃𝑦 ∈
𝐴 (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵)) |
10 | 7, 8, 9 | 3bitr4i 303 |
. . . 4
⊢ (𝑧 ∈ (∪ 𝐴
∩ 𝐵) ↔
∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵)) |
11 | | vex 3474 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
12 | 11 | inex1 5311 |
. . . . . . 7
⊢ (𝑦 ∩ 𝐵) ∈ V |
13 | | eleq2 2818 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∩ 𝐵) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑦 ∩ 𝐵))) |
14 | 12, 13 | ceqsexv 3522 |
. . . . . 6
⊢
(∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ 𝑧 ∈ (𝑦 ∩ 𝐵)) |
15 | | elin 3961 |
. . . . . 6
⊢ (𝑧 ∈ (𝑦 ∩ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵)) |
16 | 14, 15 | bitri 275 |
. . . . 5
⊢
(∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵)) |
17 | 16 | rexbii 3090 |
. . . 4
⊢
(∃𝑦 ∈
𝐴 ∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵)) |
18 | | rexcom4 3281 |
. . . 4
⊢
(∃𝑦 ∈
𝐴 ∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑥∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥)) |
19 | 10, 17, 18 | 3bitr2i 299 |
. . 3
⊢ (𝑧 ∈ (∪ 𝐴
∩ 𝐵) ↔
∃𝑥∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥)) |
20 | 4, 5, 19 | 3bitr4ri 304 |
. 2
⊢ (𝑧 ∈ (∪ 𝐴
∩ 𝐵) ↔ 𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 ∈
𝐴 𝑥 = (𝑦 ∩ 𝐵)}) |
21 | 20 | eqriv 2725 |
1
⊢ (∪ 𝐴
∩ 𝐵) = ∪ {𝑥
∣ ∃𝑦 ∈
𝐴 𝑥 = (𝑦 ∩ 𝐵)} |