Metamath Proof Explorer

Theorem iinin2

Description: Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use intiin to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion iinin2 ⊢ A ≠ ∅ → ⋂ x ∈ A B ∩ C = B ∩ ⋂ x ∈ A C

Proof

Step Hyp Ref Expression
1 r19.28zv ⊢ A ≠ ∅ → ∀ x ∈ A y ∈ B ∧ y ∈ C ↔ y ∈ B ∧ ∀ x ∈ A y ∈ C
2 elin ⊢ y ∈ B ∩ C ↔ y ∈ B ∧ y ∈ C
3 2 ralbii ⊢ ∀ x ∈ A y ∈ B ∩ C ↔ ∀ x ∈ A y ∈ B ∧ y ∈ C
4 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ A C ↔ ∀ x ∈ A y ∈ C
5 4 elv ⊢ y ∈ ⋂ x ∈ A C ↔ ∀ x ∈ A y ∈ C
6 5 anbi2i ⊢ y ∈ B ∧ y ∈ ⋂ x ∈ A C ↔ y ∈ B ∧ ∀ x ∈ A y ∈ C
7 1 3 6 3bitr4g ⊢ A ≠ ∅ → ∀ x ∈ A y ∈ B ∩ C ↔ y ∈ B ∧ y ∈ ⋂ x ∈ A C
8 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ A B ∩ C ↔ ∀ x ∈ A y ∈ B ∩ C
9 8 elv ⊢ y ∈ ⋂ x ∈ A B ∩ C ↔ ∀ x ∈ A y ∈ B ∩ C
10 elin ⊢ y ∈ B ∩ ⋂ x ∈ A C ↔ y ∈ B ∧ y ∈ ⋂ x ∈ A C
11 7 9 10 3bitr4g ⊢ A ≠ ∅ → y ∈ ⋂ x ∈ A B ∩ C ↔ y ∈ B ∩ ⋂ x ∈ A C
12 11 eqrdv ⊢ A ≠ ∅ → ⋂ x ∈ A B ∩ C = B ∩ ⋂ x ∈ A C