Step | Hyp | Ref
| Expression |
1 | | 19.26 1481 |
. . . 4
⊢
(∀𝑦((𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦) ∧ (𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦)) ↔ (∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))) |
2 | | elun 3276 |
. . . . . . 7
⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) |
3 | 2 | imbi1i 238 |
. . . . . 6
⊢ ((𝑦 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝑦) ↔ ((𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝑦)) |
4 | | jaob 710 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝑦) ↔ ((𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦) ∧ (𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))) |
5 | 3, 4 | bitri 184 |
. . . . 5
⊢ ((𝑦 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝑦) ↔ ((𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦) ∧ (𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))) |
6 | 5 | albii 1470 |
. . . 4
⊢
(∀𝑦(𝑦 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝑦) ↔ ∀𝑦((𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦) ∧ (𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))) |
7 | | vex 2740 |
. . . . . 6
⊢ 𝑥 ∈ V |
8 | 7 | elint 3850 |
. . . . 5
⊢ (𝑥 ∈ ∩ 𝐴
↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)) |
9 | 7 | elint 3850 |
. . . . 5
⊢ (𝑥 ∈ ∩ 𝐵
↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦)) |
10 | 8, 9 | anbi12i 460 |
. . . 4
⊢ ((𝑥 ∈ ∩ 𝐴
∧ 𝑥 ∈ ∩ 𝐵)
↔ (∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))) |
11 | 1, 6, 10 | 3bitr4i 212 |
. . 3
⊢
(∀𝑦(𝑦 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝑦) ↔ (𝑥 ∈ ∩ 𝐴 ∧ 𝑥 ∈ ∩ 𝐵)) |
12 | 7 | elint 3850 |
. . 3
⊢ (𝑥 ∈ ∩ (𝐴
∪ 𝐵) ↔
∀𝑦(𝑦 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝑦)) |
13 | | elin 3318 |
. . 3
⊢ (𝑥 ∈ (∩ 𝐴
∩ ∩ 𝐵) ↔ (𝑥 ∈ ∩ 𝐴 ∧ 𝑥 ∈ ∩ 𝐵)) |
14 | 11, 12, 13 | 3bitr4i 212 |
. 2
⊢ (𝑥 ∈ ∩ (𝐴
∪ 𝐵) ↔ 𝑥 ∈ (∩ 𝐴
∩ ∩ 𝐵)) |
15 | 14 | eqriv 2174 |
1
⊢ ∩ (𝐴
∪ 𝐵) = (∩ 𝐴
∩ ∩ 𝐵) |