Theorem: Set Intersection is Self-Distributive/Families of Sets

Let $I$ be an indexing set.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ and $\family {B_\alpha}_{\alpha \mathop \in I}$ be indexed families of subsets of a set $S$.
Then:
:$\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha} = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}$
where $\ds \bigcap_{\alpha \mathop \in I} A_\alpha$ denotes the intersection of $\family {A_\alpha}$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha \cap B_\alpha 
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B_\alpha
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcap_{\alpha \mathop \in I} A_\alpha
      | c ={{Defof|Intersection of Family}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = \bigcap_{\alpha \mathop \in I} B_\alpha
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
Thus by definition of subset:
:$\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha} \subseteq \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}$
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcap_{\alpha \mathop \in I} A_\alpha
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = \bigcap_{\alpha \mathop \in I} B_\alpha
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B_\alpha
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha \cap B_\alpha
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha}
      | c = {{Defof|Intersection of Family}}
}}
{{end-eqn}}
Thus by definition of subset:
:$\ds \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha} \subseteq \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha}$
{{qed|lemma}}
By definition of set equality:
:$\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha} = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}$
{{qed}}