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)
Does the proof of Serre's GAGA theorem use the axiom of choice? If so, at what step does this happen?