Characterization of V-stages in the absence of foundation or replacement In the absence of foundation and replacement, we can say that $x$ is an ordinal iff $x$ is hereditarily well-founded (with respect to the relation $\in$) and hereditarily transitive, where
$$ \text{$a$ is transitive} \longleftrightarrow \forall x \forall y (x \in y \in a \rightarrow x \in a) $$
Is there a similar characterization for stages of the von Neumann universe? That is, $x$ is a stage iff $\phi(x)$ for some first-order formula $\phi$? I suspect the property of being supertransitive
$$ \text{$a$ is supertransitive} \longleftrightarrow \forall x \forall y (x \subseteq y \in a \rightarrow x \in a) $$
might be useful here, but I'm not sure how to prove a definitive characterization. This would allow us to specify (in the absence of foundation and replacement) the stage $V_\alpha$ corresponding to a given ordinal $\alpha$ by saying $V_\alpha$ is the intersection of all $x$ such that $x$ is a stage and $\alpha \subseteq x$.
Edit: Let
$$ \text{$a$ is powertransitive} \longleftrightarrow \forall x \forall y (x \in y \in a \rightarrow \mathcal{P} x \in a) $$
If I'm not mistaken, $a$ is supertransitive iff $\mathcal{P} a$ is powertransitive. Can we say that $V_\alpha$ is precisely the intersection of all supertransitive, powertransitive supersets of $\alpha$?
 A: Naively you'd think that supertransitive is the right definition. Note that supertransitive simply means that $y\in a\to\mathcal P(y)\subseteq a$, which is a good starting point. After all, the $V_\alpha$'s are exactly those transitive sets which compute power sets correctly.
But your intuition is right, it is not enough without Replacement. To see why, A.R.D. Mathias noted that given any limit ordinal $\lambda>\omega$, the class $M_\lambda=\{x\mid\sup(\lambda\cap\operatorname{tcl}(x))<\lambda\}$ is a class model of Zermelo's set theory. But this model only has a von Neumann hierarchy up to $\lambda$ itself. By relative to these models, the traces of the "real" von Neumann hierarchy are supertransitive.
So supertransitive is not enough. You can revert to the actual definition by recursion. First, $\phi(x,\alpha)$ to define that $x=V_\alpha$, and then simply $\exists\alpha\phi(x,\alpha)$. So what is $\phi(x,\alpha)$? The conjunction of the following:


*

*$\alpha$ is an ordinal, and

*there is a function $f$ with domain $\alpha+1$, such that $f(0)=\varnothing$,  $f(\beta+1)=\mathcal P(f(\beta))$, and if $\beta$ is a limit ordinal, then $f(\beta)=\bigcup\operatorname{rng}f\restriction\beta$. And $x=f(\alpha)$.


But of course, this is not what you want. You want to have some internal property. So instead of this, you need to require that in addition to being well-founded and supertransitive, there are no $\alpha+1$-sequences in $\in$. Namely, for any function $f\colon\alpha+1\to x$, there is some $\beta<\gamma$ such that $f(\beta)\notin f(\gamma)$.
