If every set has a well order, then the axiom of choice follows:
Given a well order on $\bigcup_{i \in I} A_i$ we define the choice function in this way $f(i) =$ "the first element of $\bigcup_{i \in I} A_i$ that is also in $A_i$".
Now I'm trying to write down this formula in a ZF fashion.
I could say:
$f:=\{(i,y)\in I\times (\bigcup_{i \in I} A_i) \ | $ $y$ is the first element of $\bigcup_{i \in I} A_i$ in $A_i$ $\}$.
But I would like to go deeper using the definition of binary relation and well ordering.
Any suggestion?
Suppose that $R$ is the well-order on $\bigcup_{i\in I}A_i$, then $f(i)=\min_R A_i$ is a neat way of writing that. Another would be:
$$\varphi(i,a):=a\in A_i\land(\forall b\in A_i)(\langle a,b\rangle\in R\lor a=b)$$
Of course if you want to be strict about it, then $\{A_i\mid i\in I\}$ and $R$ are parameters in the formula.