I'm trying to prove the equivalence between two different statements of the Axiom of Choice (presented below as AC1 and AC2). I'd like to know if my proof is correct (also presented below).
One concern I have is the following: is it necessary to prove that the set $\{B_i\}_{i\in I}$ (as described in the proof below) can be defined? And if this is the case, did I prove that point correctly?
Another concern I have is about the converse proof: can I just assume that the range of a given function is a set that exists, or do I need to specify that I'm applying the axiom of replacement to get such set?
Aside from these concerns, I'm also open to any other correction and suggestion you'd like to give. Thank you everybody in advance.
AC1. Let $I$ be a non-empty set, and let $\{S_i\}_{i\in I}$ be a pairwise disjoint family of non-empty sets indexed by $I$. There exists a set $C$ such that $|C\cap S_i|=1$ for all $i\in I$. Such set is called the choice set.
AC2. Let $I$ be a non-empty set, and let $\{S_i\}_{i\in I}$ be a family of non-empty sets indexed by $I$. There is function $f:I\to\bigcup_{i\in I}S_i$ such that $f(i)\in S_i$ for all $i\in I$. Such function is called the choice function.
Proof of the equivalence between AC1 and AC2:
($\Rightarrow$) Let $I$ be a non-empty set, and let $\{A_i\}_{i\in I}$ be a family of non-empty sets which is not necessarily pairwise disjoint. Since $I$ is a non-empty set and since every set $A_i$ is non-empty, the corresponding set $\{i\}\times A_i=\{(i,x):x\in A_i\}$ is also non-empty. So, the family of non-empty sets $\{B_i\}_{i\in I}$, in which $B_i=\{i\}\times A_i$ for every $i\in I$, can be defined.
It can be shown by contradiction that $\{B_i\}_{i\in I}$ is pairwise disjoint. Suppose that there exist two indices $p,q\in I$ such that $p\neq q$ and $B_p\cap B_q\neq\emptyset$. This implies that there exists an ordered pair $(x,y)$ such that $(x,y)\in B_p\cap B_q$. But then, it would be the case that $p=x=q$, which contradicts the assumption that $p\neq q$, so no such indices exist.
Now that it's been shown that $\{B_i\}_{i\in I}$ is a pairwise disjoint family of non-empty sets, AC1 can be applied to obtain the set $C$. This set is a subset of $I\times\bigcup_{i\in I} A_i$. Also, for every $(j,x)\in C$, it is the case that $j\in I$ and $x\in A_i$, and that there is no $(j',x')\in C$ for which $j=j'$ and $x\neq x'$. Thus, there exists a choice function for $\{A_i\}_{i\in I}$ that is defined by $C$.
($\Leftarrow$) Now, let $\{A_i\}_{i\in I}$ be pairwise disjoint. AC2 can be applied to obtain the choice function $f:I\to\bigcup_{i\in I}A_i$. Let $C$ be the range of $f$. Since $\{A_i\}_{i\in I}$ is pairwise disjoint, it follows that $|C\cap S_i|=1$ for all $i\in I$. Thus, $C$ is the choice set for $\{A_i\}_{i\in I}$.