picking a witness requires the Axiom of Choice? $\forall I, A:Set. I\subseteq \bigcup A\to \exists f:I\to A. \forall i\in I. i\in f(i)$
Does this theorem require the Axiom of Choice? To prove, I need to find $\forall i\in I$ a witness of that $i\in \bigcup A$. Any witness $B$ is such that $i\in B\land B\in A$. There may be more than one witness, but I must return one, a choice function will pick it. I define a function $w_S:I\to P(A), w_S(i) := \{B\in A|i\in B\}$, $w_S$ returns a set of witnesses. $im(w_S)$ satisfies the hypothesis of the Axiom of Choice, then I construct a choice function $c:im(w_S)\to A$ and return $c\circ w_S$.
The “relation→function” form of the Axiom of Choice from Equivalent statements of the Axiom of Choice is also suitable for the proof.
AFAIK if the Axiom of Choice is used in a proof, then the proof explicitly says that. But I came across some proof similar to my theorem which does not mention the Axiom of Choice, so I am unsure.
(Update 2011-03-30. My theorem above is required for this theorem: $\forall A,B:Set. finite(A) \land A\subseteq \bigcup B \to \exists B'\subseteq B. finite(B')\land A\subseteq\bigcup B'$ which intuitively is “every finite set is compact”. It is implicitly used here, theorem 3.2.2.)
(Update 2011-03-31. It turned out that my theorem is not required for the theorem in “Update 2011-03-30”. That is a good example to learn in what cases the Axiom of Choice is required.
I rewrote Apostolos's proof:
Proof. Assume that $X$ is a set of inhabited sets. Define $i(b) := \{B\in X | b\in B\}\cup\{\{b\}\}, dom(i)=\bigcup X$. Assume that $i(b_0)=i(b_1)$, then $\{b_0\}\in i(b_1)$, then $(\{b_0\}\in X \land b_1\in\{b_0\}) \lor b_0=b_1$, left disjunct also implies $b_0=b_1$. Then $i$ is an injection. Then $i:\bigcup X\to im(i)$ is a bijection. Assume that $B\in X$, then $B$ is inhabited, take $b, b\in B$, by definition of $i$ $B\in i(b)$, obviously $i(b)\in im(i)$. Then $X\subseteq (im(i))$. By my theorem, take $w:X\to im(i)$. By $i$ being a bijection, define $c:X\to\bigcup X, c := i^{-1}\circ w$. Assume that $B\in X$, then $w(B) = i(c(B))$, then by definition of $w$ $B\in w(B)$, then by definition of $i$ and $c$ $c(B)\in B$.  Then $c$ is a choice function. Qed.)
 A: This is equivalent to the axiom of choice. Take a set $X$ of non-empty sets. Let the set $X'= X\cup\{\{x\} : x\in\bigcup X\}$ and for every $x\in\bigcup X$ take $C_x=\{y\in X' : x\in y\}$. Observe that if $x\neq y$ then $C_x\neq C_y$ since $\{x\}\in C_x$ while $\{x\}\notin C_y$. The set $A=\{C_x : x\in\bigcup X\}$ is a set through the axiom of replacement and you have that $\bigcup A=X'$. If there is a function $f:X'\to A$ satisfying the statement you wrote you have a choice function $g$ for $X$, namely $g(y)=x\iff f(y)=C_x$.
The fact that the axiom of choice is enough to show the statement you wrote is easy.
A: Yes, this requires the axiom of choice. Suppose that $\mathcal{C}$ is any family of nonempty sets. Take the family 
$$
\mathcal{D} = \{ \{X, \langle X, a\rangle\} : X \in \mathcal{C}, a \in X \}
$$
where $\langle \cdot,\cdot\rangle$ denotes an ordered pair. Note that $\langle X,a\rangle \not = X$ for all sets $X,a$ if we use the usual definition of an ordered pair in set theory. 
Now $\mathcal{C} \subseteq \bigcup \mathcal{D}$, because each set in $\mathcal{C}$ is nonempty. Assuming your principle holds, let $f \colon \mathcal{C} \to \mathcal{D}$ be such that $X \in f(X)$ for each $X \in \mathcal{C}$. Then we can define a choice function $g$ on $\mathcal{C}$ with the rule: $g(X)$ is the unique set $a$ such that $\langle X,a\rangle \in f(X)$.  This definition does not require the axiom of choice because $g(X)$ can be defined explicitly. 
