I need a global choice function defined by a formula in (a fragment of) ZF. There is no harm in assuming V=L for my purposes. But I wonder if there are any familiar alternative ways to get this?