Bounded Quantifiers in a Proof In a solutions manual for Jech's "Introduction to Set Theory", we find the following proof for $f\left[ \bigcap_{a\in A} F_a \right]\subseteq \bigcap_{a\in A}f\left[ F_{a}\right]$.
\begin{align}
y\in f\left[ \bigcap_{a\in A}F_{a}\right]&\iff \exists x\in \bigcap_{a\in A}F_{a}\text{ such that } (x,y)\in f\quad &(1)\\
\\
&\iff \forall a\in A, x\in F_{a}\text{ such that }(x,y)\in f\quad &(2)\\
\\
&\implies \forall a\in A, y\in f[F_{a}]\quad &(3)\\
\\
&\iff y\in \bigcap_{a\in A}f[F_{a}]\quad &(4)
\end{align}
The transition from (1) to (2) seems a bit unusual. How can (1) and (2) be expressed in more elementary logical terms?
 A: It would help if you explained what you find unusual about the transition from (1) to (2). 
I do think line (2) is poorly worded, since the quantifier on $x$ disappears, and it appears that $x$ is being quantified after $a$. I would write instead $$\exists x \,\forall a\in A, x\in F_a \text{ and } (x,y)\in f.$$
Does that make things clearer? I doubt things can be expressed in any more elementary way. The assertion $$x\in \bigcap_{a\in A}F_a$$
is equivalent to the assertion $$\forall a\in A, x\in F_a.$$

Edit: The goal here is to prove the implication $y\in f[\bigcap_{a\in A}F_a] \implies y\in \bigcap_{a\in A} f[F_a]$. The converse, $y\in \bigcap_{a\in A}f[F_a] \implies y\in f[\bigcap_{a\in A}F_a]$ is not true in general.
You can look at this as coming down to the fact that for any statement $\phi(x,a)$ involving $x$ and $a$, $\exists x \,\forall a\, \phi(x,a)$ implies $\forall a\,\exists x\, \phi(x,a)$, but not conversely. This is what happens in the step from (2) to (3).
$$(\exists x, \forall a\in A, x\in F_{a}\text{ and }(x,y)\in f) \implies (\forall a\in A, \exists x, x\in F_a\text{ and } (x,y)\in f)$$
The statement on the right is easily equivalent to $$\forall a\in A, y\in f[F_a]$$
A: In (1), it is saying that there is some $x$ in the intersection $\bigcap_{a\in A}F_a$ such that $(x,y)\in f$. That is, such that $f(x)=y$. That this $x$ exists follows from the hypothesis. 
By definition of intersection, $x\in\bigcap_{a\in A}F_a$ if and only if $x\in F_a$ for each $a\in A$.
When I was first learning this stuff, I liked to switch the index to $i$. For some reason, it just helped me wrap my head around it. As well, I liked to make an example with a specific index set. For instance, here we could write (1) as $x\in\bigcap_{i=1}^n F_i$ just to get something more concrete. By definition, $x\in\bigcap_{i=1}^nF_i$ if and only if $x\in F_i$ for each $i=1,2,\dots,n$.
In summary, the jump from (1) to (2) is just by definition of intersection.
Writing the proof out more wordily,

Let $y\in f\left[\bigcap_{a\in A}F_a\right]$. Then there exists $x\in\bigcap_{a\in A}F_a$ such that $y=f(x)$. By definition of intersection, this is equivalent to saying that for all $a\in A$, this $x$ is in $F_a$. Thus for all $a\in A$, $y\in f[F_a]$. By definition of intersection, this is equivalent to saying that $y\in \bigcap_{a\in A}f[F_a]$.

A: Expression $(2)$ in the original really seems incorrectly written down: as another answer says, the $\;\exists x\;$ should not have been left out.
Here is the same proof using Dijkstra/Gries/etc.'s calculational proof format and logic/set notations, which hopefully should explain all the steps, and make the structure of the proof clear.
\begin{align}
& y \in f \left[ \langle \cap a : a \in A : F_a \rangle \right] \\
\equiv & \;\;\;\;\;\text{"definition of $\;\cdot[\cdot]\;$"} \\
& \langle \exists x : y  = f(x) : x \in \langle \cap a : a \in A : F_a \rangle \rangle & (1) \\
\equiv & \;\;\;\;\;\text{"definition of $\;\cap\;$ quantification"} \\
& \langle \exists x : y  = f(x) : \langle \forall a : a \in A : x \in F_a \rangle \rangle & (2) \\
\Rightarrow & \;\;\;\;\;\text{"logic: $\;\exists\forall \Rightarrow \forall\exists\;$"} \\
& \langle \forall a : a \in A : \langle \exists x : y  = f(x) : x \in F_a \rangle \rangle \\
\equiv & \;\;\;\;\;\text{"definition of $\;\cdot[\cdot]\;$"} \\
& \langle \forall a : a \in A : y \in f\left[ F_a \right] \rangle & (3) \\
\equiv & \;\;\;\;\;\text{"definition of $\;\cap\;$ quantification"} \\
& y \in \langle \cap a : a \in A : f\left[ F_a \right] \rangle & (4) \\
\end{align}
