The OP's argument seems to be just that you cannot always construct a choice function.
But the entire point of the axiom of choice is to say "that's fine; you're still allowed to use 'unconstructed' choice functions in your proofs".
Would the OP reject the statement "let x be an element of the set of numbers that cannot be defined with finitely many symbols"; such a statement does not depend on the AoC, but I think the OP complains about making even a single choice.
But the entire point of the axiom of choice is to say "that's fine; you're still allowed to use 'unconstructed' choice functions in your proofs".
Would the OP reject the statement "let x be an element of the set of numbers that cannot be defined with finitely many symbols"; such a statement does not depend on the AoC, but I think the OP complains about making even a single choice.