Axiom. choice
∃f. choice_function f ∧ dom f = UnivCl \ {∅}