Metamath Proof Explorer

Theorem intun

Description: The class intersection of the union of two classes. Theorem 78 of Suppes p. 42. (Contributed by NM, 22-Sep-2002)

Ref Expression
Assertion intun ⊢ ⋂ A ∪ B = ⋂ A ∩ ⋂ B

Proof

Step Hyp Ref Expression
1 19.26 ⊢ ∀ y y ∈ A → x ∈ y ∧ y ∈ B → x ∈ y ↔ ∀ y y ∈ A → x ∈ y ∧ ∀ y y ∈ B → x ∈ y
2 elunant ⊢ y ∈ A ∪ B → x ∈ y ↔ y ∈ A → x ∈ y ∧ y ∈ B → x ∈ y
3 2 albii ⊢ ∀ y y ∈ A ∪ B → x ∈ y ↔ ∀ y y ∈ A → x ∈ y ∧ y ∈ B → x ∈ y
4 vex ⊢ x ∈ V
5 4 elint ⊢ x ∈ ⋂ A ↔ ∀ y y ∈ A → x ∈ y
6 4 elint ⊢ x ∈ ⋂ B ↔ ∀ y y ∈ B → x ∈ y
7 5 6 anbi12i ⊢ x ∈ ⋂ A ∧ x ∈ ⋂ B ↔ ∀ y y ∈ A → x ∈ y ∧ ∀ y y ∈ B → x ∈ y
8 1 3 7 3bitr4i ⊢ ∀ y y ∈ A ∪ B → x ∈ y ↔ x ∈ ⋂ A ∧ x ∈ ⋂ B
9 4 elint ⊢ x ∈ ⋂ A ∪ B ↔ ∀ y y ∈ A ∪ B → x ∈ y
10 elin ⊢ x ∈ ⋂ A ∩ ⋂ B ↔ x ∈ ⋂ A ∧ x ∈ ⋂ B
11 8 9 10 3bitr4i ⊢ x ∈ ⋂ A ∪ B ↔ x ∈ ⋂ A ∩ ⋂ B
12 11 eqriv ⊢ ⋂ A ∪ B = ⋂ A ∩ ⋂ B