The following is a well known result
Theorem: the axioms of $\textsf{ZFC}$ hold at (and above) the following levels of the von Neumann hierarchy:
- all levels (i.e. $V_{\alpha}$ for all $\alpha \in \text{On}$): extensionality, foundation, union, choice, separation;
- limit ordinals: powerset, pairs;
- ordinals greater than $\omega$: infinity;
- at worldly cardinals: replacement.
It wasn't clear to me how we ought to show this for choice. (Note the version of choice assumed here is important; I take the 'choice set' version rather than the 'choice function', as the latter only holds at limits.)
In some sense how this proof works is to assume $\textsf{ZFC}$ 'in the background' then see which sets inhabit each level of the hierarchy (we know 'a priori' that $\omega$ exists, what we're checking is whether it is in $V_{\alpha}$ or not): if this view is fine then it's clear enough how choice holds (take the choice set $\mathcal{C}$ for a set in $V_{\alpha}$ and note that its elements are all therefore from $V_{\beta}$ for $\beta < \alpha$, thus $\mathcal{C} \subset V_{\beta}$, and so $\mathcal{C} \in V_{\alpha}$).
Is this reasoning OK? The only alternative I can see is somehow giving the construction of $\mathcal{C}$ for an arbitrary set (which is a problem choice is there to solve in the first place$\ldots$