Mathematicians do consider "just pick an arbitrary element" sufficient. This is baked into the system of "first order logic" - the standard use of existential q

Mathematicians do consider "just pick an arbitrary element" sufficient. This is baked into the system of "first order logic" - the standard use of existential quantifiers in logic allows for proofs that make any finite number of arbitrary choices, but the proof gets longer as the number of arbitrary choices increases (so a straightforward attempt to prove that you could make an infinite sequence of arbitrary choices, in first order logic, would lead to an infinitely long proof). The first order logical system behind modern mathematics is both powerful, and limited, in this very particular strange way. You could definitely come up with alternative logical systems to first order logic where "just pick an arbitrary element" is not considered a valid proof strategy, but this would be more an exercise in philosophy and logic than in mathematics. There are good practical reasons for mathematicians to like classical first order logic (such as the fact that Godel's completeness theorem applies to it), so it would be hard to convince most mathematicians to switch to any other logical system. Making classical first order logic weaker makes it unpleasant for the purposes of getting things done for not enough benefit (although intuitionists will fight you over this claim), while trying to make it stronger leads to problems where your logical system needs to magically give you access to truths which are uncomputable in order to be complete ("abstract model theory" tries to make this claim precise). The trouble is that first order logic doesn't have a built-in concept of "infinity", let alone a rule that says it is valid to "just pick an arbitrary infinite sequence", let alone the full strength of the axiom of choice (which applies even to sets so large that their elements can't be listed via a "sequence"). Such a logical rule can only be added in a logical system which can talk about arbitrary sets or infinite sequences in the first place, which goes beyond first-order logic. So rather than having this rule be a rule of pure logic, the workaround is to add it as a mathematical axiom that applies to the (first order) mathematical theory of sets, which is meant to be a practical approximation to the (ungraspable) "true" collection of rules for "higher order logic".