# choosing elements from the set of sequences in ZFC

In my previous question, I asked about infinite-length formula in ZFC. But I am still confused over following:

Suppose you want to build a function from a set of sequences to a set that chooses $n$th element in each sequence in the set of sequences to form a new set with each chosen element as an element in the new set.

But how can I do this nicely in ZFC? Or is this impossible?

-

If $A$ is a set of sequences of elements from $X$ (that is, $A\subseteq X^{\mathbb N}$), then just take
$$\{ f(n) \mid f\in A \}$$
You can justify the existence of this by the axiom of replacement applied to $A$ and the function $f\mapsto f(n)$.
You do not even need replacement. This is a subset of $X$ definable with parameters, so comprehension suffices. – Andrés E. Caicedo Mar 23 '14 at 0:03
@Andres: Sure, but since we have replacement, might as well use it, when it's closer to the intuition we want to capture. And it also works when there's no common $X$. – Henning Makholm Mar 23 '14 at 1:17