The main problem is taking a statement about a set ("for every A in X, A is nonempty") to the existence of a set ("there is a function f [which in ZFC is consid

The main problem is taking a statement about a set ("for every A in X, A is nonempty") to the existence of a set ("there is a function f [which in ZFC is considered to be a set] such that for all A in X, f(A) is in A"). If you are able to create a statement P(A,a) that for every A in X is true for exactly one a in A, then it follows from the axiom of replacement that there is such a choice function. The axiom of choice seems to say that it suffices to make a statement P(A,a) that for every A in X is true for at least one a in A. The axiom of replacement helps actually construct such a choice function, whereas the axiom of choice just asserts one ought to exist since "at least one" seems good enough. To use the axiom of replacement, you have to use some structure for A. For instance, with the finite set example, it might be that each A is not just a set, but a set which is in bijective correspondence with a natural number, where there is a distinguished bijection. Then, you could just say that P(A,a) is true exactly when a is the image of 0 under the bijection.