ConsiderThe idea of definable separation and definable replacement may be much weaker than one expects, because they can hold vacuously. For example, consider the integers with their successor relation: $$\langle \mathbb{Z},\varepsilon\rangle,$$ where $n\mathrel{\varepsilon} (n+1)$ and these are the only instances of the relation. In this model, every set has exactly one element, its predecessor.
Since this structure has nontrivial automorphisms by translation, which move every point, it has no definable elements. It consequently satisfies vacuously all the definable axioms you mentionof set theory: definable pairing, definable power set, definable separation, definable replacement, definable union. It also satisfies full extensionality and full foundation.
This structure also satisfies what I find to be a natural version of the infinity axiom, which asserts, "there is a set containing all the finite von Neumann ordinals." The reason is that this structure has no transitive sets and therefore no objects that would be finite von Neumann ordinals; so every object contains them all vacuously as elements, and thus it also satisfies. So this structure satisfies a version of the infinity axiom.
SoBut you stated your infinity axiom to require a set whose elements are exactly the finite von Neumann ordinals, and this theory doesassertion is not interpret ZFC andtrue in the consistency strengthstructure.
Indeed, since your infinity axiom implies explicitly that there is very weakat least one definable set, you will get the empty set from it by an instance of separation and therefore also $\{\emptyset\}$ and so on. And you will get $P(\omega)$ and iterations of this, and so ultimately there will be some actual set theory going on in your theory after all.