I think the commenter means that just because you know an element with a certain property is in the set, we can't conclude that there is a way to "choose" such an element. All we know is there exists at least one of these elements, there could be one (in which case we have a choice function that is well defined, choose the one element that satisfies the property) or there could be infinitely many such elements and we're stuck back at the beginning to construct a choice function.
Edit: I think the above might be wrong actually, I haven't had a proper set theory course yet but it looks like "existential instantiation" [0] is what allows you to "choose" the element here (possibly?) but this sits within the logic that proceeds ZF set theory.
Also see [1] for a decent discussion on AOC for finite sets.
Essentially, we're not actually choosing an element from the set. We're defining a new symbol, and saying that it could represent any element in the set. But you can use that symbol pretty much as if it was one particular, but unknown, element of that set.
If I have understood this correctly, then if you "choose" some element a from a set X, and prove some proposition P(a), then you have really proved that for all e in X, P(e).
Edit: I think the above might be wrong actually, I haven't had a proper set theory course yet but it looks like "existential instantiation" [0] is what allows you to "choose" the element here (possibly?) but this sits within the logic that proceeds ZF set theory.
Also see [1] for a decent discussion on AOC for finite sets.
[0] https://en.wikipedia.org/wiki/Existential_instantiation [1] https://math.stackexchange.com/questions/132717/do-we-need-t...