Understanding a proof of an implication of the axiom of choice Can someone please clear my doubts regarding a result concerning the axiom of choice:
Prove that (i) implies (ii) where:
(i) For every nonempty set whose elements are non empty sets there exists a choice function.
(ii) If $\{a_i\}$ is a family of nonempty sets indexed by a nonempty set $I$, then there exists a family $\{x_i\}$ with $i \in I$ such that $x_i \in a_i$ for each $i \in I$.
Here is the proof which is in my book:
Let $A$ be a collection of disjoint sets. We have $A \subset \mathcal{P}(\cup_{i \in I}a_i)$. ($\mathcal{P}$ is the power set). By (i) there exists a choice function $f$ on $\mathcal{P}(\cup_{i \in I}a_i)$. Let $b$ be the image of $A$. Pick an element $a \in A, f(a) \in a \cap b$ since $f(a) \in a$. Let $y \in b$ where $y \neq f(a)$ thus we have $y = f(a')$ where $a'\neq a$, and thus $y \in a'$. Since $a$ and $a'$ are disjoint $y \notin  a$. Thus the only element of $b \cap a$ is $f(a)$.
My doubts are:


*

*Why do we need to prove this? Won't the choice function $f$ give us the family ${f(i)}$ anyway.

*How is the existence of $A$ guaranteed?

*The choice function $f$ has what domain and co-domain? If its co-domain is $\mathcal{P}(\cup_{i\in I} a_i)$ then how is that set indexed? Or is the indexing set $\mathcal{P}(\cup_{i\in I} a_i)$?

*How does $b \cap a$ being $f(a)$ guarantee that (ii) holds.
Thanks a lot.
 A: Let $\{a_i\}_{i\in I}$ be a family of sets, indexed by the nonempty set $I$.
Then by the Axiom Schema of Replacement, $S:=\{a_i\mid i\in I\}$ is a set.
By assumption and $I\ne \emptyset$, the set $S$ is a nonempyty set of nonempty sets.
By (i) there exists a choice function, i.e. a function $f\colon S\to \bigcup S$ such that $f(x)\in x$ for all $x \in S$.
For $i\in I$ let $x_i=f(a_i)$.
Then $\{x_i\}_{i\in I}$ is a family with the required properties.
A: The statement says, essentially, that if you can choose then you can choose in a somewhat one-to-one fashion. 
The assertion (ii) seems a bit weird for me, perhaps you wish to include the assumption that the family is a family of pairwise disjoint sets? The proof seems to assume that...
About the proof, you assume that $A$ is given to you. Note that every set $A$ is a subset of $\mathcal P(\bigcup A)$, this is not hard to check. Using the assumption that every collection of non-empty sets admits a choice function we simply use a choice function on $\mathcal P(\bigcup A)\setminus\{\varnothing\}$, and by the assumption that $A$ is a collection of pairwise disjoint sets we have that $\{f(a_i)\}$ is our beloved family of singletons.
