Why is the Axiom of Choice not needed when the collection of sets is finite?
It's a matter of the basic rules of inference allowed in proofs.
Suppose $\mathcal B$ is a "collection" of bins with only one element, i.e., $\mathcal B = \{S\}$ for some set $S$. The assumption is that $S$ is nonempty. By definition, this means there exists $x \in S$. We can use the existential instantitation rule of inference to fix $x \in S$. Then the association $$\mathcal B \to \bigcup_{T \in \mathcal B} T = S$$ given by $$\{S \mapsto x\}$$ defines a choice function.
Similarly, one can prove by induction that if $\mathcal B$ is a finite collection of nonempty buckets, then a choice function exists - if $\mathcal B_n$ is a collection of $n$ nonempty buckets, then fixing $S \in \mathcal B_n$, it follows that $\mathcal B_n \setminus \{S\}$ is a collection of $n-1$ nonempty buckets.
The axiom of choice says precisely that if $I$ is a set and, for each $i \in I$, we have a non-empty set $X_i$, then the product $\prod_{i \in I} X_i$ is non-empty. (Elements of products can be identified with choice functions, so non-emptiness of the product is equivalent to existence of a choice function.) When $I$ is finite, this is a statement which can be proved by induction on $|I|$, which does not require choice.
This is a good question; the main answer is that making a single choice out of a single bin is a matter of logic.
Specialized to this particular situation, if $S$ is a set and you have proven $\exists x : x \in S$, then logic allows you to introduce a new constant symbol (say, $a$) along with the corresponding an axiom $a \in S$.
The usual interpretation of this mechanic is that $a$ represents a 'choice' of an element of $S$, although this is by no means the only way to interpret this sort of thing:
- We might instead interpret $a$ as simply being a dummy variable, so that what we're doing is defining a function of $S$
- We might interpret $a$ as some sort of 'generic' element of $S$ rather than a choice of a specific element
- Some forms of logic allow you to introduce $a \in S$ even when $S$ is an empty set; naturally this does not lend itself well to interpreting $a$ as a choice of an element!
Whatever way we look at it, we can use it to prove we can make a choice from a single bin in set theory; the main steps are
- Introduce $a \in S$
- Show $\{ (S, a) \}$ is a choice function on $\{ S \}$
Whatever our philosophical opinions on logic are, this construction defines a function
$$ S \to \operatorname{ChoiceFunctions}(\{ S \}) $$
where $\operatorname{ChoiceFunctions}(X)$ means the collection of all choice functions on $X$. This, together with the hypothesis that $S$ is nonempty, implies that $\operatorname{ChoiceFunctions}(\{ S \}) $ is nonempty as well.
Finite choice is basically the same. In an ad-hoc fashion you could repeat this sort of argument by repeatedly introducing one variable at a time. Alternatively (in set theory) you can set up a recursive definition and show finite choices can be made by induction; IIRC the proof is straightforward, but complicated.