Is Extreme Parameter Free ZFC equivalent to ZFC?

Question

This question is closely connected to the following paper and to a prior question posted to Mathoverflow titled "Can Cantor's theorem be proved in Paraemter Free Zermelo",

https://wwwmath.uni-muenster.de/u/rds/ZFC_without_parameters.pdf

That paper provided an answer to a question about whether $\text{ZFC}^o$ is equivalent to $\text{ZFC}$, where $\text{ZFC}^o$ is the theory axiomatized by axioms of Extensionality, Foundation, Pairing, Union, Power, Infinity and a Parameter free version of Replacement and Separation denoted by $\text{Repl}^o$, $\text{Aus}^o$ respectively; where the axioms of Pairing, Union and Power are written in full, i.e. one can prove existence the sets $\{a,b\}$; $\bigcup a$; $\mathcal P(a)$ for any sets $a,b$ using those three axioms and Extensionality without using an instance of schema of specification.

In the Wikipedia, axioms of $\text{ZFC}$ are written in a different manner, see the following link:

https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory

The axioms of Pairing, Union, Power and Replacement only asserts existence of a non specific set that contains sets $a,b$ ; elements of elements of $a$; subsets of $a$, replacements of elements of $a$ respectively; one needs to use Specification in order to prove existence of the sets $\{a,b\}$; $\bigcup a$; $\mathcal P (a)$, $F(a)$

Now if by $\text{eZFC}^o$, denoting $\text{"extreme Parameter Free ZFC"}$, it is meant $\text{ZFC}$ axiomatically presented as how it is mentioned in the Wikipeida but with Specification and Replacement axioms replaced by parameter free versions of them, i.e. by $\text{Repl}^o$ and $\text{Aus}^o$ with these two schemata being formalized exactly as in the above-mentioned article (see: Postscript) for full exposition of $\text {eZFC}^o$. Then apparantly the proof presented in the above article fails, because it clearly depends on specifying pairs, unions, powers and replacment sets without the need to use Specification, and thus in some manner it allows the use of Parameters external to Specification scheme. Along the same line $\text{eZC}^o$ denotes $\text{"extreme Parameter Free Zermelo"}$, and this is $\text{eZFC}^o$ minus Replacment.

Given that, the questions are:

Is $\text{eZFC}^o$ equivalent to $\text{ZFC}$?

Is $\text{eZC}^o$ equivalent to $\text{ZC}$?

If both are false then is Cantor's theorem provable in $\text{ZFC}^o$ or $\text{ZC}^o$?

---

PS: $\text{eZFC}$ is formulated in the first order language of set theory with the following axioms:

Extensionality: $\forall A,B (\forall X (X \in A \iff X \in B) \iff \forall Y (A \in Y \iff B \in Y))$

Foundation: $\forall A (\exists X \in A \implies \exists B \in A (\not \exists C \in B (C \in A)))$

Specification: if $\phi$ is a formula in which only symbol $X$ occurs free, then

$\forall A \exists B \forall X (X \in B \iff X\in A \wedge \phi)$

is an axiom.

Pairing: $\forall A,B \exists C (A \in C \wedge B\in C)$

Union: $\forall A \exists B \forall X,Y (X \in Y \wedge Y \in A \implies X \in B)$

Power: $\forall A \exists B \forall X (\forall Y \in X (Y \in A) \implies X \in B)$

Replacement: If $\phi(Y,Z)$ is a formula in which only symbols $Y,Z$ occur free, then:

$\forall A \exists B \forall X (\exists Y \in A (\forall Z (\phi(Y,Z) \iff Z=X)) \implies X \in B)$

is an axiom.

Infinity: $\exists X (\varnothing \in X \wedge \forall Y \in X (\{Y\} \in X))$

$\text {+\-}$

$AC$

Answer 1

The answer is to the negative for both questions. A result proved by Levy. This can be seen in Kanamori's article: Levy and set theory. Annals of Pure and Applied Logic 140 (2006) 233–252

In page 247, he wrote:

Levy’s main, negative results addressed another issue of self-refinement in axiomatics and showed that his aforementioned positive result is reasonably sharp. In the presence of Separation the generative axioms are sometimes given parsimoniously in a weaker, conditional form, e.g. $\forall u \exists y \forall x (x \subseteq u \to x \in y) $ for the Power Set Axiom. With his positive result, the set $\sf T $ consisting of the usual $\sf ZF$ axioms, but with the Separation schema replaced by $S_0$ and the Replacement schema replaced by the conditional version, is an axiomatization of $\sf ZF$. Levy established that full Separation is not a consequence of $\sf T$ if the Power Set axiom is weakened to the conditional form. He also established the analogous results for the conditional version of Union and the conditional version of Pairing.

[Note: $S_0$ is the same as $\text{Aus}^o$ here]

Answer 2

Since Replacement can be proved from parameter-free Replacement (a theorem of Azriel Levy), and Separation can be proved in full from Replacement, the answer is that if we have parameter-free Replacement, and $\sf ZF$ without Replacement and Separation, then we can prove Replacement, and therefore Separation as well.

Azriel Levy, "Parameters in the comprehension axiom schemas of set theory", in: Leon Henkin et al. (Eds.), Proceedings of the Tarski Symposium, in: Proceedings of Symposia in Pure Mathematics, vol. 25, American Mathematical Society, Providence, 1974, pp. 309–324.

Asking about Zermelo (which I presume means $\sf ZF$ without Replacement, but with Separation) amounts to your previous question about parameter-free separation.