The question I'm asking here is purely technical. For the below mentioned theory, can it be defined in first order logic with equality and membership, or it necessitates adding '$\operatorname {stage}$' as a primitive one place predicate symbol to that language.
Axioms
Extensionality: $X \subset Y \land Y \subset X \implies X=Y$
Foundation: $,\exists x: \phi(x), \implies \exists x: \phi(x) \land \forall y \, (\phi(y) \implies y \not\in x)$,
where '$y$' does't occur free in $\phi(x)$, and $\phi(y)$ is the formula obtained from $\phi(x)$ by merely replacing all occurrences of the symbol '$x$' by the symbol '$y$'.
Define: $\operatorname {stage} (X) \iff \\ \forall y \ [y \in X \iff \exists Y (\operatorname {stage} (Y) \land Y \subsetneq X \land y \subseteq Y)] $
Separation: $\exists x: x=\{y \in A \mid \phi\}$; if '$x$' is not free in $\phi$.
Hierarchy: $\forall x \exists \operatorname {stage} S: x \in S$
Infinity: $\exists X: X \neq \emptyset \land \forall x \in X \, (\{x\} \in X)$