The difference to the axiom of choice is that in the antecedent, the existence of
The principle is important but as an axiom it is of interest merely for theories that have weak comprehension and the capability to encode functions.
This is the case, for example, in some weak constructive set theories[1] or some higher-order arithmetics.
Restrictions to the complexity of the predicate may be considered, for example only quantifier-free formulas may be allowed.
Set theoretically, the existence of a particular codomain may be part of the formulation.
In arithmetic frameworks, the functions can be taken to be sequences of numbers.
If a proof calculus includes the principle of excluded middle, then the notion of function predicate is a liberal one as well, and then the function comprehension principle grants existence of function objects incompatible with the constructive Church's thesis.
So this triple of principles (excluded middle, function comprehension, and Church's thesis) is inconsistent.
Adoption of the first two characterizes common classical higher order theories, adoption of the last two characterizes strictly recursive mathematics, while not adopting function comprehension may also be relevant in a classical study of computability.
Indeed, the countable function comprehension principle need not be validated in computable models of weak, even classical arithmetic theories.
and some weaker theories, unique choice is also derivable.
As in the case with theories of arithmetic, this then means that certain constructive axioms are strictly constructive (anti-classical) in those theories.
Arrow-theoretic variants of unique choice can fail, for example, in locally Cartesian closed categories with good finite limit and limit properties but with only a weakened notion of a subobject classifier.