Using Axiom of Replacement to construct the set of sets that are indexed by a set I'm now reading the proof of Mitchell's embedding theorem proved in the book of Swan 'Algebraic K-Theory'.
Now I'm trying to understand the sentence

'It is well known that for a small abelian category $A$, the functor category from $A$ to the category $Ab$ of abelian groups is well powered, right complete, and has injective envelopes.'

To understand the well-poweredness, I tried to understand that for a functor $F$, $\{ F(X) \}_{X \in \mathrm{obj}(A)}$ is a set.
I guess the relevant axiom in the set theory is the 'Axiom of Replacement' and it seems that the axiom is understood to be natural because if a collection of elements of a class is indexed by a set, then the collection is also a set because the cardinality of the collection is bounded by the index set. With this explanation, $\{ F(X) \}_{X \in \mathrm{obj}(A)}$ must be a set.
But in the textbooks of set theory, there is a mention of the definable property (more precisely definable in the formal first order language) in the axiom of replacement.
So my question is
In the category theory, do we implicitly assume that a functor is definable? or if not the argument using the cardinality is formal enough?
(By the way, If you can also briefly explain the sentence of the Swan's book, then that would be also a great help! as I'm not meant to be a specialist in this field.)
 A: In the Axiom of Replacement, the "definition" involved is allowed to use parameters, i.e. it is allowed to refer to specific sets.  In this case, the functor $F$ is a set, and so your definition using Replacement is allowed to refer to $F$.
(Note that if $A$ were not small, then it would not be possible for a functor on $A$ to be a set (though in some special cases it may be possible to "encode" such functors with sets).  In that case, working in ZFC, it would not be possible to quantify over such functors at all and formulate a theorem such as the one you refer to.  Instead, you would need to work in a set theory that can refer to "large" objects as described in Pace Nielsen's answer.)
A: For category theory, rather than using ZFC as the background theory, one usually works with an axiomatic system that treats classes a little more simply, like NBG.  In NBG, the axiom of replacement has no definability requirement for class functions.
If you want to stick with ZFC, then yes you are implicitly assuming that functors are class functions, and hence are definable from first-order formulas in the language (possibly with set parameters).
I personally like to work with ZFC + an axiom of universes.  In this view, one may take every category to be contained in a universe.  Thus, every functor is actually a set, and hence definable (using that set as a parameter).
A: Another way to formalise functors from a small category $A$ to a large concrete category $C$ is to define it as a function $El(F) \to Ob(A)$, where the preimage of $a\in Ob(A)$ is precisely the underlying set of the value of $F$ at $a$, together with some more data specifying the effect of arrows (plus a functoriality condition). In one sense this is defining away the problem, but in fact such an approach is necessary when dealing with these kind of functors in other settings.
For functors to $\mathbf{Ab}$, you would specify that the fibres of $El(F) \to Ob(A)$ are equipped with an abelian group structure, and that the functoriality data respects that.
In this way, no universes are needed, and the data is, informally, exactly what you think it should be.
