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$



Is Extreme Parameter Free ZFC equivalent to ZFC?
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](http://math.bu.edu/people/aki/11.pdf). 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]


