The replacement axiom (axiom scheme) is the most general form you need, essentially saying that if you have a function whose domain is a set then the image is also a set. Furthermore, the empty set can be inferred by an existence of any set at all, when combined with separation (and hence, can be inferred by replacement).
Formally speaking the replacement schema says that for every formula $\varphi(u,v,p_1,\ldots,p_n)$, fix the parameters $p_1,\ldots,p_n$ and pick any set $A$, whenever $u\in A$ has at most one $v$ for which $\varphi(u,v,p_1,\ldots,p_n)$ is true, then the collection of $\{v\mid\varphi(u,v,p_1,\ldots,p_n), u\in A\}$ is also a set.
How to infer separation and pairing? Simple.
First we infer separation. Given $\phi(x)$, we simply define $\varphi(u,v,p)$ to be $$\varphi(u,v,p)\stackrel{\text{def}}{=} u=v\land u\in p\land\phi(u)$$
This is a functional formula (i.e. for every $u$ there is at most a single $v$ for which $\varphi(u,v,p)$ holds) and it is easy to verify that the image of $\varphi(u,v,a)$ is indeed $\{x\in a\mid \phi(x)\}$.
The empty set exists by separation - simply take some $a$ (which exists because we assume there is some set in the universe) and the function $\phi(x)\colon = x\neq x$.
As you noted, $\{\emptyset ,P(\emptyset)\}$ exists by the Power set axiom.
Now for a given $x,y$ we want to have $\{x,y\}$ so we define the following $\varphi(u,v)$ as following:
$$\varphi(u,v) \colon = (u=\emptyset\wedge v=x)\vee (u=P(\emptyset)\wedge v=y)$$
Note that $\varphi$ is a functional formula, i.e. for a given $u$ there is only one $v$ for which $\varphi(u,v)$ is true. By the axiom of replacement we have now that $\{x,y\}$ is a set. Therefore the axiom of pairing holds if we assume Power set and Replacement.
Now we have two ways of looking at ZFC. Sometimes we want to prove that something is a model for ZFC and need to verify the list of axioms in which case proving both Separation and Replacement is completely redundant. At other times we want to prove certain things which are quicker when using the more specific axioms (e.g. pairing (or even ordered pairing, which can be quickly inferred from pairing itself)).
This is a sort of freedom that we allow ourselves. We add extra axioms that we don't really need. Then if we want to ensure all the axioms hold we check for the "core" of the axiomatic system, and when we want to ease on ourselves in other cases we can just use the extra axioms for our convenience.
The reflection principle is a theorem schema in ZFC, meaning that for each formula $\phi(\vec x)$ we can prove in ZFC a version of the principle for $\phi$. In particular, it gives us that if $\phi$ holds (in the universe of sets) then there is some ordinal $\alpha$ such that $V_\alpha\models \phi$.
It follows from this that (assuming its consistency) $\mathsf{ZFC}$ is not finitely axiomatizable. Otherwise, $\mathsf{ZFC}$ would prove its own consistency, violating the second incompleteness theorem. The (standard) list of axioms you presented is actually an infinite list, with replacement being in fact an axiom schema (one axiom for each formula).
It is perhaps worth mentioning that no appeal to the incompleteness theorem is needed: If $\mathsf{ZFC}$ is consistent, and finitely axiomatizable, then it would prove (because of reflection) that there are $\alpha$ such that $V_\alpha\models\mathsf{ZFC}$. It would then follow that there is a least such $\alpha$. But inside $V_\alpha$ there must be some $\beta$ such that $$V_\alpha\models\mbox{``}V_\beta\models\mathsf{ZFC}\mbox{''}$$
(because $V_\alpha$ is a model of set theory, so it satisfies reflection), and easy absoluteess arguments give us that then $\beta<\alpha$ is indeed an ordinal, and $V_\beta$ is really a model of $\mathsf{ZFC}$, contradicting the minimality of $\alpha$.
Best Answer
I haven’t read this work of Jech, but it seems you are under a few misconceptions.
Replacement is not indexed by “all functions”. A function is an object discussed in ZFC, so it does not make sense to say there is one axiom per function. Instead, replacement is indexed over “properties” in the same way separation is.
Formally, consider any formula $P(x, y, w_1, \ldots, w_n)$ - that is, a formula $P$ in the language of set theory such that every variable which occurs free in $P$ is one of $x, y, w_1, \ldots$, or $w_n$. The instance axiom of replacement for $P$ states
$$\forall w_1 \cdots \forall w_n \forall a (\forall x \in a \exists! y P(x, y, w_1, \ldots, w_n) \implies \exists b \forall y (y \in b \iff \exists x \in a P(x, y, w_1, \ldots, w_n)))$$
It is clear that because there are only countably many such $P$, there are only countably many instances of replacement. It is also clear that deciding whether a particular sentence is an instance of the axiom scheme of replacement is decidable. The same is true for deciding whether a sentence is an instance of the axiom scheme of separation. Therefore, whether a sentence is an axiom of ZFC is decidable.
For the rest of the discussion, we assume ZFC is consistent.
We can encode sentences in the language of arithmetic into the language of set theory in such a way that makes ZFC an extension of Peano Arithmetic. Because ZFC is a recursively axiomatisable consistent extension of Peano Arithmetic, there is no algorithm which can decide whether a particular sentence can be proved in ZFC.
Finally, ZFC cannot be finitely axiomatised. There is a powerful principle called the “reflection principle”, which states that for all sentences $\phi$, ZFC proves that there is some transitive set $S$ such that $(S \models \phi) \iff \phi$. So for any list $A_1, \ldots, A_n$ of axioms of ZFC, we can prove in ZFC that there is some model of $\phi := A_1 \land A_2 \land \cdots \land A_n$, and thus the combination of axioms $A_1, \ldots A_n$ is consistent. If ZFC were finitely axiomatisable, then it would prove itself consistent, which is impossible by Gödel’s second incompleteness theorem.
So the set of axioms of ZFC is countably infinite and decidable, and we can’t cut the axioms down to a nice finite list while still having all the theorems of ZFC.