The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi all,

Is the axiom of choice required if all sets have one only element ?
If not, how to prove it ?

Russel said that if all sets contain a pair of socks, we need the axiom
of choice to select a sock in each pair but that if they are shoes,
we don't need it, because the choice function can be : "take the left
shoe".

But for sets of one only element ?

Namely, I want to prove :
   (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x)

Is is possible, or do I need the fucking axiom of choice ?

Thanks.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/