Serre's GAGA result roughly states the following. Let $X$ be a complex projective algebraic variety. Then the natural functor from the category of coherent sheaves over the algebraic structure sheaf of $X$ to the category of coherent sheaves over the analytic structure sheaf of $X$ is an equivalence of categories.

This theorem always seemed to have the air of magic to me. Things that are analytic must come from algebra. I want to dust away some of this magic, and get a clearer picture. With this goal in mind, I have skimmed the proof of GAGA.

The proof of GAGA is rather involved. It uses Cartan's theorem A for both the algebraic and analytic cases, the isomorphism of the completions of the stalks of the structure sheaf in the algebraic case and the analytic case, and a variety of technical results. After having done that for a few days, I still remain with a sense of amazement and a basic lack of understanding about what makes this work. This brings me to the precise phrasing of my question: (which will hopefully help me find the precise step where the magic happens)

### Question

Does the proof of Serre's GAGA theorem use the axiom of choice? If so, at what step does this happen?