Why does ZFC need an axiom schema of specification?

Solution 1:

Let $\alpha$ be any limit ordinal. Let's study the structure $(\alpha,\in)$.

1. It satisfies Extensionality, as any linear order does.
2. It satisfies Power Set, since if $\beta\in\alpha$, the only subsets of $\beta$ which are elements of $\alpha$ are other ordinals, so $\beta+1$ is the power set of $\beta$.
3. If $\alpha>\omega$, then Infinity also holds.
4. Separation fails: the only object which does not contain the empty set (as an element!) is the empty set itself, and so $\varphi(x)=\exists y(y\in x)$ is a fairly simple formula, but $\{x\in\beta\mid\varphi(x)\}$ is not a set, as far as $\alpha$ is concerned, whenever $\beta\geq2$.

So, you see, Power Set does not imply Separation. It is true, however, that Replacement implies Separation. And so it is, in some sense redundant. Once we get into weaker set theories, however, this redundancy becomes helpful. Which is one of the reasons it stuck around for so long.