Let $X$ be a D11: Set.
Let $E_n$ be a D11: Set for each $n \in \mathbb{N}$ such that
Let $E_n$ be a D11: Set for each $n \in \mathbb{N}$ such that
| (i) | $\bigcup_{n \in \mathbb{N}} E_n$ is the D77: Set union of $E = \{ E_n \}_{n \in \mathbb{N}}$ |
Then
\begin{equation}
\bigcup_{n \in \mathbb{N}} E_n
\subseteq X
\quad \iff \quad \forall \, n \in \mathbb{N} : E_n \subseteq X
\end{equation}