Can one exhibit an explicit Kuratowski infinite set without invoking Replacement? The customary formulation of the Axiom of Infinity within Zermelo-Fraenkel set theory asserts the existence of an inductive set: a  set  $ I$ with  $\varnothing\in  I$  such  that $x\in I$ implies $x\cup\{x\}\in I$.  Since the intersection of any nonempty set of inductive sets is itself inductive, an instance of  the Axiom Schema of Separation implies the existence of  a smallest inductive set, namely the set of von Neumann naturals $$\mathbb{N}_{\bf  vN} = \{\varnothing, \{\varnothing\},\{\varnothing,\{\varnothing\}\},\ldots\}.$$
Any inductive set is infinite (in fact, Dedekind infinite) but this formulation of the axiom  asserts more, namely the existence of a specific countably infinite set.  Given one such set, the existence of others, for example  the set of  Zermelo naturals $$\mathbb{N}_{\bf Zer}=\{\varnothing,\{\varnothing\},\{\{\varnothing\}\},\ldots\}$$  follows from appropriate instances of the Axiom Schema of Replacement. 
Consider the subsystem of  Zermelo-Fraenkel set  theory  with axioms Extensionality, Separation Schema, Union, Power Set, Pair.  Augment  this  Basic System with  an  Axiom of Infinity which asserts the existence of an infinite set, but not any particular one. Such a  formulation requires that the notion of 'finite' be defined prior to that of 'natural number',  following Kuratowski for example.  Any infinite set $ I$ determines a Dedekind-infinite  set of local naturals $$\mathbb{N}_I=\{\mbox{equinumerosity classes of finite  subsets of }  I\}$$ which (duly equipped with initial element and  successorship) yields a  Lawvere natural  number  object, as  in  the Recursion  Theorem. The  existence of  $\mathbb{N}_{\bf vN}$ and $\mathbb{N}_{\bf Zer}$ then follow from  appropriate instances of Replacement.
One might wonder  if  there is some clever way to specify an infinite  set without  recourse to Replacement. That is, does there exist (in the  language of set  theory)   a formula $\boldsymbol \phi$
with one  free variable  $x$ such  that
$$ \mbox{Basic+Infinity+Foundation } \vdash\; \exists y ( \forall  x (x\in y \leftrightarrow \boldsymbol \phi)\,\wedge \, y \mbox{ is  infinite})\>?$$
I'm inclined  to  guess no, on the following circumstantial  grounds:


*

*For  $\mathbb{N}_{\bf vN}$ and $\mathbb{N}_{\bf Zer}$  the  use of Replacement  is  essential: Mathias has shown (Theorem 5.6 of Slim  Models of Zermelo Set Theory  that there exist transitive models ${\mathfrak  M}_{\bf  vN}$ and ${\mathfrak M}_{\bf Zer}$  of Basic+Infinity+Foundation with  ${\mathbb  N}_{\bf vN}\in {\mathfrak M}_{\bf vN}$  and ${\mathbb  N}_{\bf Zer}\in{ \mathfrak M}_{\bf Zer}$, but  such  that every  element  of ${\mathfrak M}_{\bf  vN}\cap {\mathfrak M}_{\bf Zer}$  is hereditarily finite.

*The usual  definitions  of  $\mathbb{N}_{\bf vN}$ and $\mathbb{N}_{\bf Zer}$  involve unstratified formulas. Coret has shown (Corollary 9 of  Sur les cas stratifiés du schéma du replacement) that this is unavoidable:
$$ \mbox{Basic+Infinity } \vdash\; \forall y ( \forall  x (x\in y \leftrightarrow  \boldsymbol \phi)\,\rightarrow \, y \mbox{ is  hereditarily finite})$$
for any stratified  $\boldsymbol \phi$. Using  the  same technique he has shown  (Corollary 10) that  Basic+Infinity proves  every stratified instance of Replacement.
 A: The answer is no. Let ZC' be ZFC without replacement and infinity and with the assertion there is a Kuratowski infinite set. We will construct a model $M$ of ZC' such that only hereditarily finite elements of $M$ are fixed under all automorphisms of $M.$ The idea is generate a model from a $\mathbb{Z}^2$-array of objects, each of whose only element is the object below it in the array.
Define $M=\bigcup_{m<\omega} \bigcup_{n \in \mathbb{Z}} \mathcal{P}^m(\{\omega\} \times \mathbb{Z} \times [n, \infty)),$ where we adjust the $\mathcal{P}$ operator to replace each singleton of the form $\{(\omega, n_1, n_2)\}$ with $(\omega, n_1, n_2+1).$ (We use $\omega$ to differentiate the $\mathbb{Z}^2$ objects from the hereditarily finite sets).
Define a relation $E$ on $M$ by $E \restriction \mathbb{Z}^2=\{((\omega, n_1, n_2),(\omega, n_1, n_2+1)): n_1, n_2 \in \mathbb{Z}\}.$ Extending $E$ to the iterated power sets is done in the natural way. It is easy to see $(M, E)$ satisfies ZC'.
Notice that the map $(\omega, n_1, n_2) \mapsto (\omega, n_1, n_2+1)$ extends to a unique automorphism on $M,$ which only fixes hereditarily finite elements. Thus, none of the infinite sets in the model are first-order definable.
Update: The author of this question was curious whether there is such a model which also satisfies transitive containment (TC), the assertion that every set has a transitive closure. The answer is yes; here's a sketch of such a model.
Assume ZFC + "there are non-OD reals" in $V$ (or work in a ctm satisfying a sufficiently large finite fragment of this theory). We'll build an OD model $M$ of ZC'+TC such that, from every infinite element $x,$ we can define (in $V$) a non-OD real $r.$ Then $x$ is not definable in $M,$ or else we would have an ordinal definition for $r.$
For $r \in \mathbb{R} = \mathcal{P}(\omega),$ we recursively define $n_r$ by $0_r=\emptyset$ and $(n+1)_r =\{n_r\}$ if $n \not \in r,$ and $(n+1)_r = \{n_r, \emptyset\}$ if $n \in r.$ Basically, we're defining a new system of natural numbers for each real.
Let $M = \bigcup_{m=0}^{\infty} \bigcup_{S \in [\mathbb{R} \setminus OD]^{<\omega}} \mathcal{P}^m ( \{n_r: n<\omega, r \in S\} ).$
For each infinite $x,$ there are finitely many (and at least one) non-OD reals $r$ such that the transitive closure of $x$ contains every $n_r.$ The least such real is as desired. And it's routine to verify $M \models ZC'+TC.$
