The constructible universe satisfies AC

Let $a\in L$ be internally a family of nonempty sets. Transitivity makes every $b\in a$ an actual nonempty subset of L. Inside L, separate the restriction of its canonical order to b; this is a well-order by F1, so b has a unique least element $m(b)\in b$. The rule specifying m is one fixed internal formula, with no chosen ordering parameter.

Internal Replacement applied to $b\mapsto ⟨b,m(b)⟩$ produces a graph $g\in L$ with domain a, since internal Pairing in F4 constructs the ordered pairs. The uniqueness in step 1.1 makes g a function and $g(b)\in b$ for each $b\in a$. If a is empty this graph is empty. Thus g is the choice function required by F5. AC was proved internally; it was not invoked to choose the least elements.