Axiom of Choice: Where does my argument for proving the axiom of choice fail? Help me understand why this is an axiom, and not a theorem.
When you move from $\exists s\in S$, to specifying "Let $s$ be an element of $S$" you are using what is known as existential instantiation. This is an inference rule of the underlying logic, stating that if there are objects satisfying some property, we can add a new symbol to the language with the statement that this symbol satisfies our property.
So you can apply it once, or twice, or thrice, and if you live long enough and all you do is apply it, then maybe even a few trillion times. Sure, all that is fun and games. But how can you apply it to each and every set of real numbers?
You simply can't.
So what you did there, really, was to say that you have a function mapping $S$ to an element of itself, and that this was your uniform existential instantiation. But why would such a function exist? Well, the answer is that without postulating its existence, it is possible that no such function exists. So you need to have the axiom of choice to assert the existence of such a function, which happens to be exactly what the axiom of choice is doing: it allows you to take all those sets, and get existential instantiation for all of them for the price of one; namely, you only need to instantiate the quantifier stating "There exists a choice function" once, and the rest is given.
Let me add two remarks here.
Zermelo, historically, treated the axiom of choice as a principle of logic, rather than an axiom of set theory. Probably to do exactly what you did there.
Many modern proof assistants prove the axiom of choice, by exactly the same argument as this. When you eliminate existential quantifiers like this uniformly, you simply get a choice function. This is not a bug per se, it's more of a consequence of the design features.
This is a confusing matter, mainly because the kind of reasoning you use in your proof is usually taken to be valid.
However, in order to formalize that reasoning in axiomatic set theory, we need to reduce it to particular symbolic formulas in a formal logic system. And it turns out that the rules of symbolic logic and set theory that are sufficient to express most other kinds of generally accepted proofs can't by themselves express your reasoning.
We declare that this is not the fault of your reasoning, but of the limited logical rules we already have. Then we set out to fix our axiomatic set theory by adding a new rule stating that it's allowed to do what you do. This new rule is the axiom of choice.
So the problem with your proof is not that it doesn't work, from the perspective of ordinary mathematics -- but that what it does is not very interesting. It just says that if we accept this kind of reasoning, then we must conclude that this kind of reasoning works, which doesn't really tell us anything.
What a "proof of the axiom of choice" ought to be would be an argument that even if we don't extend our system with this new rule, we can still prove everything we can prove with the rule. But that means that the proof has to be done with fewer tools than we normally allow ourselves to use.
Otherwise, the end result would be something like claiming that you don't need to buy a hammer for your toolbox, because you can still drive in nails. How? Well, just hit the nail with a hammer ...
This is a misunderstanding about the essence of axiomatic set theory. In axiomatic set theory, you don't assume that a set exists because you can think of it; in a sense, the entire point of axiomatic set theory is not to do that, to decouple the notion of existence of sets from such pre-existing (pun intended) notions.
When you say "Define $f(S)=s$", you're already assuming that $f$ exists. The point of the axiom of choice is to allow you to deduce the existence of $f$ from the axioms. If this seems unnecessarily formal, consider that before the advent of axiomatic set theory it probably seemed unnecessarily formal to ask whether the set of all sets that don't contain themselves exists. What do you mean, does it exist? Just define $A=\{x\mid x\text{ is a set that doesn't contain itself}\}$!