Why do we even need axiom schema? It has already been shown that a parameter-free form of ZFC is as strong as ZFC with parameters (hence it is not necessary to have a separate axiom for every list of parameters). Even so, comprehension remains an axiom schema because $\forall\varphi.\forall X.\exists Y.\forall y.y\in Y\iff(y\in X\land \varphi(y))$ cannot be a first-order formula if $\varphi$ is a predicate.

But then, I'm told that ZFC is single-sorted and that the only terms are sets. Furthermore, predicates can be represented as sets by way of $\varphi(x)\iff x\in S_\varphi$, where, naturally $S_\varphi=\{x:\varphi(x)\}$; and this is done specifically to avoid introducing new sorts (or types) to set theory.

That being the case, why bother with the axiom schema at all?

Why not have the single axiom $\forall P.\forall X.\exists Y.\forall y.y\in Y\iff (y\in X\land y\in P)$?

The same thing can be done with replacement.



Edit:

To clarify, my thinking goes something like this:

Technically, $\{x:\varphi(x)\}$ is, in general, a class but not a set. That being said, if $X$ is a set and $S_\varphi$ is a class, and $z\in Z\iff z\in X\land z\in S_\varphi$, then $Z$ is also a set. ZFC is single-sorted, so the distinction between set and class is not explicit. In fact, the only way to formally prove the statement "$X$ is/is not a set" is to introduce additional sorts to ZFC.

If you extend ZFC by classes (obtaining a two-sorted theory), then the axiom above can be "translated" to:

$$\forall P^\mathbf{class}.\forall X^\mathbf{set}.\exists Y^\mathbf{set}.\forall y^\mathbf{set}.y\in Y\iff(y\in X\land y\in P)$$

(which is basically the same as the second order axiom of comprehension)

The reason I didn't think this was necessary is that there oughtn't be any set $X$ such that $X$ is the intersection of a set and class (the latter of which cannot be proven to exists in ZFC), but is not the intersection of a set with another set.

Let $\varphi$ be a predicate such that $\{x:\varphi(x)\}$ is a class but not a set. Unless the class $\{x:\varphi(x)\}\cap\mathbf{set}$ is empty, then there must be some set $Y$ such that for any set $X$, $X\cap Y$ is equivalent to $X\cap\{x:\varphi(x)\}$, yes?

Why should it matter if $\{x:\varphi(x)\}$ provably exists?
$S_\varphi$ need not be a set as you defined it : take $\varphi(x) := (x=x)$ for instance. So you need to have some form of thing that tells you that when you restrict it to $X$, then it is in fact a set. 

That's what the comprehension axiom scheme tells you. The same type of thing happens with replacement.

In fact it's a theorem that (assuming it's consistent) ZFC cannot be finitely axiomatized : you really do need some axiom schemes, otherwise you're strictly less powerful.

So we can't get rid of axiom schemes if we want to get ZFC, no matter how smart we are in formulating things (as long as we're doing things in the first order, and assuming ZFC is consistent)
Summary/takeaway of discussion

The axiom schema of comprehension guarantees that for any set $X$ and predicate $\varphi$, there exists a set $Y$ containing those members of $X$ for which $\varphi(x)$ holds.

In a particular extension of ZFC:


Every set is a class (but not every class is a set)
For every predicate $\varphi$, there is a class $C_\varphi$ such that $x\in C_\varphi\iff \varphi(x)$


For a given $\varphi$, the axiom of comprehension can be stated as:

$$\forall X.\exists Y.\forall y.y\in Y\iff(y\in X\land \varphi(y))$$

This is equivalent to:

$$\forall X.\exists Y.\forall y.y\in Y\iff (y\in X\land y\in C_\varphi)$$

Since the class of sets exists, if the intersection $C_\varphi$ with the class of sets is nonempty, then there is a least set $S_\varphi$ such that $\varphi(s)$ holds for all $s\in S_\varphi$ (this is not something proven within the scope of the theory, it's just a generic statement).

Since each predicate has a corresponding set, we can rewrite the above as:

$$\forall S.\forall X.\exists Y.\forall y. y\in Y\iff (y\in X\land y\in S)$$

This is equivalent to "the intersection of any two sets exists."

Moving back to ZFC, we can take away classes entirely by assuming $\{x:\varphi(x)\}$ to be the least member of the intersection of $C_\varphi$ with the class of sets (this guarantees at least one set for each predicate). If $S_\varphi$ is the least such set, then the above guarantees that for any set $X$, the set $\{x\in X:\varphi(x)\}=X\cap S_\varphi$ exists.

However, this does not prove that $S_\varphi$ exists.

So while we might be able to prove that "every subset of the integers exists" (provided that we can prove the existence of the integers), we cannot prove that "the set of odd integers exists".

This is where the "axiom of intersection," as it were, fails. While it suffices to prove that a subset of a particular set exists if there is a second set to take the intersection, it does not prove that the second set exists in the first place.

Proving the existence of the second set ultimately requires proving that for any $\varphi$, $S_\varphi$ exists - ultimately ends up being equivalent to the original axiom schema of comprehension.



For anyone who's interested, it might be possible to produce interesting "fragments" of ZFC by replacing the axiom schemata as described, and adding a "set construction axiom" (basically, an algorithm for constructing new sets from existing ones, for example $\forall x.\exists y. y=\{x\}$).

I don't know what applications this would have, if any, but it's something to think about.