Defining a set which contains one element per element in another set I'm doing a bunch of topology exercises at the moment, and one thing I sometimes want to express is "given set $X$, let $Y$ be a set which contains an element per element in $X$". As an example, here's an attempted proof that second-countable spaces are Lindelöf:

Let $X$ be a second-countable topological space. Let $\mathcal B$ be some countable basis for its topology. Let $\mathcal C$ be an open cover of $X$. Let $\mathcal B'=\{B\in \mathcal B:\exists C\in \mathcal C\text{ such that }B\subseteq C\}$.
Let $\mathcal C'$ be a subcover of $\mathcal C$ which for each $B\in \mathcal B'$ contains one $C\in \mathcal C$ such that $B\subseteq C$.

What bothers me is the last line. It feels like it could have been more readable with set builder notation, but how do I express it?
 A: How about this:
Let $\alpha:\mathcal B'\to\mathcal C$ be a function sending each $B\in\mathcal B'$ to some $C\in\mathcal C$ sthat satisfies $B\subseteq C$.
Now let $\mathcal C'$ be the image of $\alpha$, i.e. $\mathcal C'=\{\alpha(B)\mid B\in\mathcal B'\}$.

Actually $\alpha$ is a "choice function".
A: This is an application of the Axiom of Choice. One of its formulations (there are several equivalent ones) is that when we have any family of non-empty sets $A_i, i \in I$ then there is a so-called choice function $f: I \to \bigcup_i A_i$ such that $f(i) \in A_i$ for all $i$. This AC is what's needed to justify your proof (within set theory):
In your case you have defined $\mathcal{B}' = \{B \in \mathcal{B}: \exists C \in \mathcal{C}: B \subseteq C\}$.
Then for each fixed $B \in \mathcal{B}'$ we can consider the set $\mathcal{C}(B):=\{C \in \mathcal{C}: B \subseteq C\}$ which is a non-empty subset of $\mathcal{C}$, by definition, as $B \in \mathcal{B}'$ and so we have a choice function $f: \mathcal{B}' \to \mathcal{C}$ such that $f(B) \in \mathcal{C}(B)$ for all $B \in \mathcal{B}'$, so in particular $B \subseteq f(B) \in \mathcal{C}$. 
In this case we "only" need the countable version of choice (i.e. for countable families) as $\mathcal{B}'$ is countable being a subset of $\mathcal{B}$, the countable base. 
The final step is to note that $\{f(B): B \in \mathcal{B}'\}$ is a countable subcover, i.e. the only thing left to check is that it still covers $X$.
To this end, let $x \in X$. Then there is some $C_x \in \mathcal{C}$ that contains $x$ and as $\mathcal{B}$ is a base and we have an open cover, there is also some $B_x \in \mathcal{B}$ with $x \in B_x \subseteq C_x$. This shows that $B_x \in \mathcal{B}'$ (it has a superset in $\mathcal{C}$) and so $f(B_x)$ is a set in our subcover, and we know that $B_x \subseteq f(B_x)$, so $f(B_x)$ also covers $x$. As $x$ was arbitrary, we are done.  
