$\omega$ is a set I'm trying to show from the $ZFC$ axioms that $\omega$ is a set and I have something that I think could be a proof but I'm not sure about one of its parts. In particular, I want to use the axiom that says the range of a definable function is a set. But I think definable means that the function can be expressed as a formula in $L_S$ and I can't see how to do that. Here's what I have:
The axiom of Infinity is the following: $$\exists x ( x \neq \varnothing \land \forall y ( y\in x \rightarrow y \cup \{y\} \in x))$$
By Infinity there is an infinite set, $U$. Pick any $u$ in $U$. Now define a function $f$ that maps $u$ to $\varnothing$ (which exists by Empty Set). Map the successors as follows: $s(u) \mapsto s(\varnothing)$ and so on. 
This "and so on" is the part that I'm not sure about: I think I have to write $f$ in a first order formula in $L_S$. Since I didn't manage, alternatively, I was wondering if the following (less satisfactory) argument would do: Use that Choice is equivalent to the principle of recursive construction and define $f(s(u)) = s (f(u))$.
To finish apply Replacement to obtain that the range $\omega$ of $f$ is a set.
Many thanks for your help.
 A: Usually the axiom of infinity is usually stated: 
$(\exists x)(\emptyset \in X \wedge (\forall y \in x)(y \cup \{y\} \in x))$
see Kunen's $\textit{Set Theory}$ (2011) or Jech's $\textit{Set Theory}$.
Any set $x$ which has the above property is called an inductive set. Then $\omega$ is defined to be the intersection of all inductive sets. Notice that in this form of the axiom of infinity and the definition of an inductive set $\emptyset \in X$. 
You can also show that if you define the natural numbers as the von neumann ordinals, the axiom of infinity is equivalent to the existence of the set of all natural numbers which is equivalent to the existence of any limit ordinal. 

Now to show your form of infinity is equivalent to form above. 
It is clear that the form above implies your form. Now to show that your form implies the form above. Let $x$ be such a set given by your form of the axiom of infinity. $x$ has a relation $\in$ on it. $\in$ is set like, well-founded (by the axiom of foundation), and extensional (by the axiom of extensionality). Then $mos$, the Mostowski collapsing function, is an $\in$ preserving bijection with the transitive set $mos(x)$. $\emptyset \in mos(x)$. Since $x$ has the property that for all $y \in x$, $y \cup \{y\} \in x$ and the fact that $mos$ is a $\in$-preserving bijection, $mos(x)$ has the property that whenever $y \in mos(x)$, $y \cup \{y\} \in mos(x)$. Hence I have shown there is an inductive set containing $\emptyset$ (which you were worried about existed in the comments). Hence you have my form of the axiom of infinity. Now you can defined $\omega$ to be the intersection of all inductive sets containing $\emptyset$. 
