Bounded definition of omega ($x=\omega$)

In ZF, $\omega$ is the least nonzero limit ordinal. Ordinality is expressed by a bounded formula in set theory asserting transitivity and strict total membership order, with well-foundedness supplied by the Axiom of foundation. Put $L(x)=\mathrm{Ord}(x)\wedge x\ne \varnothing \wedge \forall y\in x\exists z\in x(y\in z)$. Then $x=\omega$ is equivalent over ZF to $L(x)\wedge \forall y\in x\neg L(y)$, again bounded. Therefore nested transitive models of ZF have the same $\omega$.