Axiomatic ZFC Set Theory Can the Axiom Schema of Comprehension be omitted from ZFC since it is implied by the Axiom Schema of Replacement?
 A: Yes.
However, historically (prior to the earliest axiomatizations of set theory) it used to be almost the other way round.  Comprehension, as we understand it today, allows to construct subsets of other sets based on a formula; in earliest (and inconsistent) set theories it was used to construct sets out of the blue.  This is sometimes called "unlimited comprehension" and it can be consistently introduced into some fuzzy set theories (that is, set theories not built on classical, two-valued logic).  Unlimited comprehension had to disappear from mainstream mathematics with the discovery of set theoretic paradoxes.
I'm not going to state mathematically what exactly gets implied by unlimited comprehension in classical logic (well, everything does), but I can still claim that in early Cantor's work, many principles that later appeared as separate axioms of ZF were seen (as a matter of course) as direct applications of unlimited comprehension: axiom of sum, power set, pairing, infinity, and of course also replacement.  In those happy days if you could write a formula that uniquely defined the membership of a set, you had that set created.
Allow me one more remark.  Comprehension isn't the only "non-essential" axiom in the traditional formulation of ZF.  Pairing follows from replacement, too.  Replacement is actually an axiom schema and many of its instances follow trivially from its other instances.  The point of the traditional "ZF" formulation is that it is easy to explain (especially as a replacement for its inconsistent, non-axiomatic predecessor framework with unlimited comprehension and extensionality as the key two principles), not that it is a minimal theory in any technical sense.
