Formal logic and functions (I am struggling with writing my proof) I wish to show that $f\left(\bigcup_aX_a\right)=\bigcup_af(X_a)$
My attempt:
$$y\in f\left(\bigcup_aX_a\right)\implies\exists x\in\bigcup_aX_a:y\in f(\{x\})$$
which I didn't like, so I re-wrote it as:
$$\forall y\in f\left(\bigcup_aX_a\right)\exists x\in\bigcup_aX_a:y\in f(\{x\})$$
I have to introduce an $x$, I need to put an exists somewhere (unlike proving De Morgan's laws, where you can just say $x\in$left hand side $\implies\in$RHS and then the other way)
Now I can write the "if $x$ is in the union of some sets it is in at least one of them" nicely as:
$$\forall x\in\bigcup_aX_a\exists b:x\in X_b$$ - given an $x$ I can get a $b$.
How do I use this above?
$$\forall y\in f\left(\bigcup_aX_a\right)\exists x\exists b:x\in X_b\implies y\in f(\{x\})$$
I am saying for all y there exists an x (based on that y) there exists a b based on that x and y with $x\in X_b$.... surely I could also say "there exists a b where there exists an x such that x in $X_b$ implies...." 
I will want to go to:
$\forall y\in f\left(\bigcup_aX_a\right)\exists b:y\in f(X_b)$ which makes me want to swap round the order of exists. 
Then from this we go (not sure how to write it with equal rigor) that y would be in the union of $f(X_a)$ over a.
Completing the proof
My first attempt:
$y\in f\left(\bigcup_aX_a\right)\implies f^{-1}(\{y\})\subset \bigcup_aX_a$ so $\exists x\in f^{-1}(\{y\})$ with $x\in\bigcup_aX_a$ which doesn't feel as concrete as I'd like.
 A: This is not a real answer, but a long comment to jdc's answer.
To be totally "formal" is an hard task, due to the huge amont of defined symbols used in set language [see as example : Yuri Manin, A Course in Mathematical Logic for Mathematicians (2010), Chapter 1.3 : Beginenrs' Course in Translation, page 9-on].
Let us try with :

$∃x \in \bigcup_a X_a (f(x)=y)$.

In order to simplify it, abbreviate the formula $(f(x)=y)$ as $\varphi(x,y)$; thus, we have (more "formally") :
$(\exists x) (x \in \bigcup_a X_a \land \varphi(x,y))$.
Now, if we have the simpler case of $X_1 \cup X_2$, our formula will be :

$(\exists x) [(x \in (X_1 \cup X_2)) \land \varphi(x,y)]$.

This is "quite" first-order logic ...
The condition $x \in (X_1 \cup X_2)$, by definition of union of sets, is equivalent to:
$(x \in X_1) \lor (x \in X_2)$.
Now, with the "$\bigcup$-case", we are not allowed to write a "potentially" infinite disjunction; thus, we have to use $\exists$.
We have that $x \in \bigcup_a X_a$ is equivalent to : 
$(\exists a) [(a \in A) \land (x \in X_a)]$, 
where $A$ is the (left implicit) index-set.
We try now to "assemble" all together :


$(\exists x) ( \quad (\exists a) [(a \in A) \land (x \in X_a)] \land \varphi(x,y) \quad )$.


Now we need a rule for quantifiers :

$\exists x P(x) \land Q \leftrightarrow \exists x (P(x) \land Q), \quad$ provided that $x$ is not free in $Q$.

In our formula above, $i$ is not free in $\varphi(x,y)$; thus we apply the rule to get :
$(\exists x) (\exists a) ( [(a \in A) \land (x \in X_a)] \land \varphi(x,y) )$.
Now we need a second rule for quantifiers :

$\exists x \exists y P(x,y) \leftrightarrow \exists y \exists x P(x,y)$.

Applying it we have :
$(\exists a) (\exists x) ( [(a \in A) \land (x \in X_a)] \land \varphi(x,y) )$.
An this is (again "omitting" the index-set) :


$(\exists a) (\exists x) [(x \in X_a) \land f(x)=y]$


that, with a little "sloppiness", we write it as :
$∃a ∃x \in X_a (f(x)=y)$.
An then we can try to go on ...
Recalling that a function in set theory is a set of ordered couples, we have that $f(x)=y$ is : 
$(x,y) \in f$
where in turn $f \subseteq X_a \times f[X_a]$.
Thus : $x \in X_a$ and $y \in f[X_a]$.
In conclusion, from : $∃a ∃x \in X_a (f(x)=y)$
we have that :

$\exists a (y \in f[X_a])$.

The last step is easy ... and I hope it can help.
A: I'm not sure what you mean by "concrete," but the following is correct.
$y \in f[\bigcup_\alpha X_\alpha]$ if and only if there exists $x \in \bigcup_\alpha X_\alpha$ such that $f(x) = y$. This happens if and only if there exists an $\alpha$ such that $x \in X_\alpha$ and $f(x) = y$, which in turn means that there is an $\alpha$ such that $y \in f[X_\alpha]$. But that means $y \in \bigcup_\alpha f[X_\alpha]$.
Given the number of things you've said above you don't like, this may or may not be anything like what you're looking for.
Edit: In the vague hope that you might like something more formal (and don't mind chaining "iff" signs in a manner that some mathematicians consider abusive), I offer the following.
\begin{align*}
y \in f\Big[\bigcup_\alpha X_\alpha\Big] &\iff 
\exists x \in \bigcup_\alpha X_\alpha \ \big(f(x) = y\big)\\
&\iff \exists \alpha\ \exists x \in X_\alpha \big(f(x) = y\big)\\
&\iff \exists \alpha\ \big(y \in f[X_\alpha]\big) \\
&\iff y \in \bigcup_\alpha f[X_\alpha].
\end{align*}
A: Using slightly different notations which I find more convenient, the statement to be proved is
$$
\tag{0} f[\langle \cup a :: X_a \rangle] \;=\; \langle \cup a ::  f[X_a] \rangle
$$
where the definitions are
\begin{align}
\tag{1} & y \in f[X] \;\equiv\; \langle \exists x : f(x) = y : x \in X \rangle \\
\tag{2} & z \in \langle \cup a :: V(a) \rangle \;\equiv\; \langle \exists a :: z \in V(a) \rangle \\
\end{align}
For me, the simplest way to prove $(0)$ is to go to the element level using these definitions, and use the laws of logic: investigate which elements are part of the left hand side, and then transform into the right hand side.

In other words, for any $\;y\;$ we calculate as follows:
\begin{align}
& y \in f[\langle \cup a :: X_a \rangle] \\
\equiv & \qquad \text{"definition (1) for $\;\cdot[\cdot]\;$"} \\
& \langle \exists x : f(x) = y : x \in \langle \cup a :: X_a \rangle \rangle \\
\equiv & \qquad \text{"definition (2) for $\;\langle \cup \ldots \rangle\;$"} \\
& \langle \exists x : f(x) = y : \langle \exists a :: x \in  X_a \rangle \rangle \\
(*) \;\;\; \equiv & \qquad \text{"logic: exchange $\;\exists\;$ quantifications"} \\
& \langle \exists a :: \langle \exists x : f(x) = y : x \in  X_a \rangle \rangle \\
\equiv & \qquad \text{"definition (1) for $\;\cdot[\cdot]\;$"} \\
& \langle \exists a :: y \in f[X_a] \rangle \\
\equiv & \qquad \text{"definition (2) for $\;\langle \cup \ldots \rangle\;$"} \\
& y \in \langle \cup a :: f[X_a] \rangle \\
\end{align}
which proves $(0)$ by set extensionality.

This proof clearly shows that the key step $(*)$ is that two nested $\;\exists\;$ quantifications (or two nested unions) may be exchanged.
