Finite product of indicator functions equals indicator of intersection

Let $X$ be a D11: Set such that
 (i) $E_1, \ldots, E_N \subseteq X$ are each a D78: Subset
Then $$\prod_{n = 1}^N I_{E_n} = I_{\bigcap_{n = 1}^N E_n}$$
Subresults
Subresult 0
Binary product of indicator functions equals indicator of intersection
Let $X$ be a D11: Set such that
 (i) $A, B \subseteq X$ are each a D78: Subset of $X$
Then $$I_A I_B = I_{A \cap B}$$
Proofs

Let $X$ be a D11: Set such that
 (i) $E_1, \ldots, E_N \subseteq X$ are each a D78: Subset
We understand both $\prod_{n = 1}^N I_{E_n}$ and $I_{\bigcap_{n = 1}^N E_n}$ as functions from $X$ to $\{ 0, 1 \}$. Since the domain and codomain sets are the same, it suffices to show that they attain the same values on $X$.

If $x \in X$, then one has the following chain of equivalencies $$\begin{split} \left( \prod_{n = 1}^N I_{E_n} \right)(x) = I_{E_1}(x) \cdots I_{E_N}(x) = 1 \quad & \iff \quad x \in E_1, \quad \dots, \quad x \in E_N \\ & \iff \quad x \in \bigcap_{n = 1}^N E_n \\ & \iff \quad I_{\bigcap_{n = 1}^N}(x) = 1 \\ \end{split}$$ The claim then follows from R2965: Indicator function is uniquely identified by its support. $\square$