The axioms of replacement and collection are some of the ‘strong’ axioms of set theory. They are not necessary for formalising ‘ordinary’ mathematics and do not hold in such basic systems as ETCS. They are necessary, however, whenever recursively constructing a set that is ‘larger’ than any set known before.
There are many variations on these axioms (which are actually axiom schemata in most systems), but any given system should only need one.
In general, these axioms apply to a binary relation that relates elements of one set to arbitrary sets. However, we do not expect that the relation itself be an object in the theory; really, we have an axiom schema with one axiom for every binary predicate of the proper form. We will write this predicate as , where stands for an elment of and stands for any set. (Note that there may well be other free variables in the predicate.)
Generally, will need to be an entire relation for the axiom to apply; that is, the axiom has as a hypothesis that, for every , there is some such that holds. In versions called ‘replacement’ instead of ‘collection’, also needs to be functional; that is, the axiom has the hypothesis that, for every , there is a unique such that holds. Thus, most of the ‘replacement’ versions only make sense if the language has a notion of equality of sets.
So much for the hypothesis of the axiom; the conclusion asserts the existence of a family of sets to which appropriate s belong. In a material set theory, we can simply state the existence of set such that certain . In a structural set theory, we state the existence of an index set , a total set , and a function such that each fibre for is equal to (or at least isomorphic to) certain . (Often we can take to be , but that does not come into the statement of the axioms.)
Section III.8 in
George Tourlakis, Lectures in Logic and Set Theory, Volume 2: Set Theory, Cambridge University Press (2003)