Choice from finitely many nonempty sets is indeed provable in standard ZF, but standard ZF is based on classical logic, which includes the law of the excluded middle.
Also, in Diaconescu's proof, the set $\{A,B\}$ cannot be asserted to be a two-element set. It admits a surjective map from, say, $\{0,1\}$, the standard two-element set, but that map might not be bijective since $A$ might equal $B$. If we had classical logic (excluded middle) available, then we could say that $\{A,B\}$ has either two elements or just one element, and it's finite in either case. But without the law of the excluded middle, we can't say that.
In intuitionistic set theory, there are several inequivalent notions of finiteness. The most popular (as far as I can tell) amounts to "surjective image of $\{0,1,\dots,n-1\}$ for some natural number $n$." With this definition, $\{A,B\}$ is finite, but you can't prove choice from finitely many inhabited sets. The second most popular notion of finite amounts to "bijective image of $\{0,1,\dots,n-1\}$ for some natural number $n$." With this definition, you can (unless I'm overlooking something) prove choice from finitely many inhabited sets (just as in classical ZF), but $\{A,B\}$ can't be proved to be finite.
(Side comment: I wrote "inhabited" where you might have expected "nonempty". The reason is that "nonempty" taken literally means that the set is not empty, i.e., that it's not the case that the set has no elements. That's the double-negation of "it has an element". Intuitionistically, the double-negation of a statement is weaker than hte statement itself. In the discussion of choice, I wanted the sets to actually have elements, not merely to not not have elements. "Inhabited" has become standard terminology for "having at least one element" in contexts where "nonempty" doesn't do the job.)
The axiom of choice, as far as 2019, and as far as "standard foundations" go, is an axiom of set theory, which is a foundation of mathematics.
You could argue that the power set axiom "just sits there in the background, lurking about, doing nothing but scaring those poor predicativists", because you use it to prove that uncountable sets exist.
Historically, however, Zermelo is known to have viewed choice as a logical principle. It can be seen as an inference rule, and this is how some second-order set theoretic proof assistant will prove choice in that sort of manner.
Regardless, progression in mathematics since 1904 moved the axiom of choice from an inference rule to a set theoretic axiom.
To the edit about group theory. Let's review for a moment where we actually need the axiom of choice in group theoretic proofs.
Since the axioms of a group cannot even decide if a model has some finite number of element, there are infinite models of any size. The axiom of choice comes in when we want to say something like "Every set carries a group structure" (which is equivalent to the axiom of choice). But this is not a statement in the language of groups, it's not even a statement about groups. It's a statement about sets.
Okay, so maybe the axiom of choice enters when we want to say that every divisible abelian group is injective, or every free abelian group is projective. Those are each equivalent to the axiom of choice. But again, these is not a statement in the language of groups. This is a "meta-theorem" about groups. The properties of projectivity and injectivity are not first-order anymore, they quantify over other groups and group homomorphisms. So this is really not something where choice enters "in the logic", but rather that the statement "exceeds the logic".
So what about this, and about all those rings and vector spaces and whatnot? Well. As with many cases, the axiom of choice is needed to produce some coherent choices. If we restrict all our attention to countable groups (i.e., define "countably injective groups" as those satisfying injectivity when all the groups involved are countable, etc.) then the axiom of choice will not be necessary anymore.
Choice, as I often said, is used to make our statement neat. Even if we mostly (or only) care about countable objects, or countably generated objects, choice makes mathematics simpler. It lets us generalize things to "all infinite objects", rather than "all countable objects" or "all well-ordered objects".
Despite all that, it's still a set theoretic axiom, and it comes into action when you move from the first-order theory of something to statements which actively involve quantifying over all possible models of a theory.
Best Answer
The axiom of choice states that given a family of non-empty sets, there is a function mapping each of those sets to an element of the set. The idea is to be able to move from $\forall a\in A\exists x(x\in a)$ to $\exists f\forall a\in A(f(a)\in a)$.
What you're talking about is existential instantiation, i.e. if $X$ is not empty, then we can "name" an element of it. There is also no $A$ and $B$ involved (and in your statement there is no information about them either). People sometimes mistake EI to be an instance of $\sf AC$, but that is not the case.
And of course, we know that LEM does not imply $\sf AC$, since we know that $\sf ZF$ is consistent with $\lnot\sf AC$ while LEM holds.