Axiom of non-choice


In constructive set theory, the axiom of non-choice is a version of the axiom of choice limiting the choice to just one.

Formal statement

If for each element of set there is exactly one such that a property holds, then there exists a function with domain that maps each element of to an element such that the given property holds. Formally, the axiom can be stated as follows:

Discussion

In ZF, this is a theorem derivable from the axiom of replacement.
In intuitionistic Zermelo–Fraenkel set theory, IZF, this statement is derivable from other axioms, since functions are defined as graphs in IZF. In this case can be defined as and it follows from the definition that it is actually a function.
The difference from the regular axiom of choice is that the choice of is unique for each.