If we have all axioms of Mac Lane set theory except Separation and add to them the schema of definable bounded separation, then would the resulting theory be equivalent to Mac Lane set theory?
Definable bounded Separation: if $\phi$ is a bounded formula in which all bounds are parameter free definable sets, and if $A$ is a parameter free definable set, then: $\{x \in A \mid \phi\}$ exists.
To write this in full, let $\psi_0,..,\psi_n$ be formulas such that each $\psi_i$ only have symbol $x_i$ occuring free; let $\phi$ be a formula not using symbol $X$ and in which all quantifiers appear as "$\in B_i$" bounded, then:
$\forall A, B_1,..,B_n \\ A= \{x_0 \mid \psi_0\}, B_1=\{x_i \mid \psi_i\},.., B_n=\{x_n \mid \psi_n\} \\ \implies \exists X: X=\{x \in A \mid \phi\}$
