Prove $\bigcap \{A,B,C\} = (A \cap B) \cap C$ This is a follow-up to a previous question where I asked how to prove $\bigcup \{A,B,C\} = (A \cup B) \cup C$.
The proof of $\bigcap \{A,B,C\}=(A \cap B)\cap C$ is mostly analogous:
\begin{align*}
x \in \bigcap \{A,B,C\} 
&\iff \left(\forall X\right) \left(X \in \{A,B,C\} \implies x \in X\right) \\
&\iff \left(\forall X\right) \left(X \in \left(\{A,B\}\cup\{C\}\right)\implies x \in X\right) \\
&\iff \left(\forall X\right) \left(\left(X \in \{A,B\}\lor X \in \{C\}\right)\implies x \in X\right) \\
&\iff \left(\forall X\right) \left(\left(\left(X=A\lor X=B\right)\lor X=C\right)\implies x \in X\right) \\
&\iff \left(\forall X\right) \left(\left(\left(X=A\lor X=B\right)\implies x \in X\right)\land\left(X=C\implies x \in X\right)\right) \\
&\iff \left(\forall X\right) \left(\left(\left(X=A\implies x \in X\right)\land\left(X=B\implies x \in X\right)\right)\land\left(X=C\implies x \in X\right)\right) \\
&\iff \left(\forall X\right)\left(\left(X=A\implies x \in X\right)\land\left(X=B\implies x \in X\right)\right)\land\left(\forall X\right)\left(X=C\implies x \in X\right) \\
&\iff \left(\left(\forall X\right)\left(X=A\implies x \in X\right)\land\left(\forall X\right)\left(X=B\implies x \in X\right)\right) \\ & \quad \quad \quad \land\left(\forall X\right)\left(X=C\implies x \in X\right) \\
& \quad \ \vdots \\
&\iff \left(x\in A \land x \in B\right)\land x\in C \\
&\iff x\in \left(A \cap B\right) \land x\in C \\
&\iff x \in \left(A \cap B\right) \cap C
\end{align*}
However, I'm unsure: how do we eliminate the universal quantifiers near the vertical dots?
Note: I know that $\cap$ is associative so I could have written $(A\cap B)\cap C$ as $A\cap(B \cap C)$, or even as $``A\cap B \cap C"$, but I am trying to be as rigorous and formal as possible with logical symbols and punctuation in this proof.
 A: I'd think of it this way:
$$
\begin{align}
x \in \bigcap \{A, B, C\} &\iff (\forall X in \{A, B, C\}) x \in X \\
&\iff (\forall X)(X \in \{A, B, C\} \to x \in X) \\
&\iff (\forall X)(X = A \vee X = B \vee X = C \to x \in X) \\
&\quad\vdots \\
&\iff (x \in A \wedge x \in B \wedge x \in C) \\
&\iff x \in (A \cap B \cap C)
\end{align}
$$
Yes there a few elisions here, but all statements are equivalent.
A: You eliminated the quantifiers just like fine.  At that point you are using the one-point rule for $\forall$:
$$
(\forall x)(x = a \implies P(x)) \;\iff\; P(a)
$$
And there is of course its dual,
$$
(\exists x)(x = a \land P(x)) \;\iff\; P(a)
$$
And there several quite similar rules, like
$$
\sum_{x=a} f(x) \;=\; f(a)
$$
etc.
The only name I've ever seen for this set of rules is "one-point rule", in the works of Edsger W. Dijkstra et al.  To make the symmetry between the above rules more explicit, they write the above more like the following:
\begin{align}
\langle \forall x : x = a : P(x) \rangle &     \;\iff\;    P(a) \\
\langle \exists x : x = a : P(x) \rangle &     \;\iff\;    P(a) \\
\langle    +    x : x = a : f(x) \rangle & \;\;\;\;=\;\;\; f(a) \\
\end{align}
(Note that their actual notations have some other differences as well; I recommend EWD1300 for an overview.)

For completeness, if you want a proof of the one-point rule for $\forall$ from other rules, here is one way:$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\ref}[1]{\text{(#1)}}
\newcommand{\then}{\implies}
\newcommand{\equiv}{\iff}
\newcommand{\followsfrom}{\Leftarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
$ for all $\;a\;$,
$$\calc
    \langle \forall x :: x = a \then P(x) \rangle
\op\equiv\hint{use antecedent $\;x=a\;$ in consequent of $\;\then\;$}
    \langle \forall x :: x = a \then P(a) \rangle
\op\equiv\hint{write $\;\phi \then \psi\;$ as $\;\lnot \phi \lor \psi\;$}
    \langle \forall x :: x \not= a \lor P(a) \rangle
\op\equiv\hint{extract disjunct not using $\;x\;$ out of $\;\forall x\;$}
    \langle \forall x :: x \not= a \rangle \lor P(a)
\op\equiv\hint{left hand side is false, witness $\;x := a\;$; simplify}
    P(a)
\endcalc$$
A: It is not really useful to drown oneself in symbols and quantifiers. One can realize that the intersection $I=\bigcap \{A,B,C\}$ is characterized uniquely by the following property:
$(1)$ It is contained in $A,B$ and $C$.
$(2)$ If $S$ is another set such that $S$ is contained in $A,B$ and $C$, $S$ is contained in $I$.
This says that $\bigcap \{A,B,C\}$ is the largest set that is contained in all three of $A,B$ and $C$. Now consider the iterated intersection $J=(A\cap B)\cap C$. Evidently it is contained in $A,B$ and $C$. Now suppose that $S$ is another set contained in $A,B$ and $C$. Then in particular $S$ is contained in $A,B$ so the defining property of $A\cap B$ says $S\subset A\cap B$. Now we see $S$ is contained in both $A\cap B$ and $C$; so the defining property of $(A\cap B)\cap C$ says that $S\subseteq (A\cap B)\cap C$. 
We have thus shown both $I$ and $J$ satisfy the same defining property stated above, and hence they must be equal.
