A 'proof' of the Axiom of Infinity Assume that the empty set $X_0$ exists.  Assume furthermore that I can form power-sets, so that I can form $X_1:=2^{X_0}$, $X_2:=2^{X_1}$, etc..  Cantor's diagonalization argument (which should not require the Axiom of Infinity) will show that $|X_m|<|X_{m+1}|$, and in particular all of these sets are distinct.  Thus, I have an infinite collection of sets.
$$X_0,X_1,X_2,\ldots $$
Now, certainly, if I list a collection of sets for you, I should be able to form the set of all things in that list, no?  How could one reasonably object that simply putting braces around things which are sets is not itself a set:
$$\{ X_0,X_1,X_2,\ldots \}$$
But, sure enough, this does not constitute a proof that the above is a set (with the usual axioms of ZF set theory (without the Axiom of Infinity itself of course)).  In fact, one cannot prove that any infinite set exists:  the hereditarily-finite sets constitute a model of ZF without Infinity.
This bothers me quite a bit for the following reason.  I view the axioms of set theory as a formalization of our intuitive notion of naive set theory, and as such, naive constructions which do not result in paradoxes  should be able to be formalized in any 'reasonable' axiomatization.  I realize this is subjective, but I suspect one would be hard-pressed to find a mathematician that seriously believed that the above construction is not 'valid', and as such, IMHO, a 'good' set of axioms would have the property that you could turn the above naive argument into a proof.
This thus yields the question:

Are there axioms for set theory which allow one to prove the existence of an infinite set without simply putting one in 'by hand'?

UPDATE:  For what it's worth, some of the comments and answers eventually had me stumble upon Tarski-Grothendieck Set Theory, which implies the Axiom of Infinity.  In some sense I suppose this technically constitutes an answer to the question, but still isn't as satisfying as one might like.
 A: The problem is how to axiomatize your assertion that

Now, certainly, if I list a collection of sets for you, I should be able to form the set of all things in that list, no? 

What do we mean by a collection of sets?  One might answer that we mean a set of sets, but that presupposes the definition of a set, and so it is unsuitable for foundational purposes.  
One might say that if we have a collection of sets $s_i$, where $i$ ranges over the elements of some set $I$, then we can form the set $\{s_i\;\colon\;i\in I\}$.  This is the Axiom of Replacement (so long as the map $i\mapsto s_i$ can be defined in your set theory).  You can use this axiom to construct the set in your question, but you do need $I$ to be a set, and in particular it should be an infinite set.  So you need the axiom of infinity.  
Perhaps we could go one step further, and say that if we have some predicate $\phi$ on sets, then we can form the set of all sets that satisfy $\phi$.  This is Frege's Axiom of (unrestricted) Comprehension.  As you probably know, this axiom is inconsistent - just take $\phi$ to be $x\not\in x$: this is Russell's Paradox.
Now, there are axiomatizations of set theory besides ZFC that try and get round this problem in different ways.  In Quine's New Foundations (NF), we are allowed to form the set $\{x|\phi\}$ as long as $\phi$ is stratifiable - loosely speaking, as long as we can assign natural numbers $l(x)$ to the variables $x$ occurring in $\phi$ such that if $x=y$ occurs in $\phi$ then $l(x)=l(y)$ and if $x\in y$ occurs in $\phi$ then $l(y)=l(x)+1$.  In particular, $x\not\in x$ is not stratifiable, so we do not run into Russell's Paradox.  
You can construct a stratifiable formula that is satisfied by your sets $X_i$, and by no other sets.  Thus, you can construct your set $\{X_1,\dots\}$ in NF.  (Update: see comments - the previous statement is untrue.  However, NF can be used to construct similar countably infinite sets.)  Indeed, the axiom of infinity is not needed in NF.  
NF is not used as often as ZFC in mathematics, and it has a few undesirable properties (for example, it does not give you a Catesian closed category of sets).  But I think it is worth keeping in mind.  
Actually, I think that the way ZFC does things is rather elegant.  In ZFC, we avoid Russell's paradox by declaring that the set of all sets is 'too large' to be a set.  Once we have the axiom of infinity, we can construct enormously large sets within ZFC, but none that are so big that they lead to a contradiction in the set theory itself.
Once we have built up our hierarchy of sets, we can use the Axiom of Replacement to carry out precisely the procedure you described.  So in ZFC, your rule is modified slightly to:

If I list a collection of sets for you, and if that collection is no larger than any set that can be constructed using the axioms of Infinity, Power Set, Union and Replacement, then I can form the set of all things in that list.

Notably, in ZFC you cannot form the set of all sets, so your original claim is untrue in ZFC, but this modified form is true.
A: Not all "collections" of sets can be sets (see e.g. Russell's paradox). If you want to be able to refer to arbitrary collections, you need a more inclusive concept such as "classes"; classes that aren't sets are called proper classes. The axiom of infinity says not only that there are infinitely many sets, but that there are sets with infinitely many elements. Your $\left\{ X_k|k\ge 0\right\}$ could be a proper class, for all we know without the axiom of infinity.
A: You could have phrased your argument differently in a much weaker logical system, namely Peano axioms.  Thus, we have the number $0$, its successor $1$, its successor $2$, etc. Doesn't that result in an infinite collection? The answer is it doesn't and in fact the existence of an infinite set has interesting foundational consequences for models of the Peano axioms.
