On ZFC, may I freely use index labelling and construct a set using function To clarify my question:
On ZFC, may I do the following freely?


*

*Given a nonempty set, label an index for each element in the set and thus construct the index set $J$.

*Given a function $f$ on a nonempty domain $D$, construct a set
$$
C := \{f(a) \mid a \in D\}.
$$
And what if I eliminate Axiom of Choice? Those above still usable?
 A: Yes, both constructions can be carried out. For (2), note that a function is really a set of ordered pairs, so its range ($C$, in your notation) is a set. If $D$ is just a subset of the domain of $f$, we can still check that $C$ is a set, using the axiom of comprehension. More generally, thanks to the axiom of replacement, if we have a first-order formula $\varphi(x,y)$ (possibly with parameters) with the property that for each $a$ in the set $D$ there is a unique $b$ such that $\varphi(a,b)$ holds, then $\{b\mid \exists a\in D\,\varphi(a,b)\}$ is a set.
Item (1) can be seen as a particular case of what we can do in (2), as just described, but in fact, (1) holds tautologically, if we choose to use as index for each element $a$ of the set $I$ the element $a$ itself (so $J=I$ and the assignment that maps each $a\in I$ to its corresponding index is just the identity, but of course we do not need to talk of functions in this particular case).
Note that choice is irrelevant in either case. Now, if what we have is a set $I$ whose elements are nonempty sets, and what we want is to label each $A\in I$ by an index $a\in A$, then this is still possible, but this is in fact the axiom of choice (the function that gives us this assignment $A\mapsto a$ is precisely a choice function on $I$), and the set $J$ is then recovered as in (2).
