Let "Injective Replacement" be the following schema:
If $\phi(x,y)$ is a formula in which only x,y occur free, and only free, then:
$\small \forall A \ [\forall x \in A \exists y (\phi(x,y)) \wedge \forall x,y,z,u (\phi(x,y) \wedge \phi(z,u) \rightarrow (x=z \leftrightarrow y=u)) \rightarrow \exists B \ \forall y \ (y \in B \leftrightarrow \exists x \in A (\phi(x,y))]$
In English, we require that the replacement function be an injection.
Now if we replace the Separation scheme in Zermelo's set theory, $Z$, by the above axiom schema, call the resulting theory "Injective Zermelo", $Z^{inj}$, then:
Would $ Z^{inj} + GCH $ interpret $ZF$ ?
Can $ Z^{inj} \pm C $ prove Cantor's theorem for an arbitrary power set?
What is the exact consistency strength of $Z^{inj} \pm C$?
Note: the rest of axioms of $Z^{inj}$ are:
Extensionality: $\small \forall A,B \ (\forall z (z \in A \leftrightarrow z \in B) \rightarrow A=B)$
Pairing: $\small \forall A,B \ \exists x \ \forall y \ (y \in x \leftrightarrow \ y=A \lor y=B)$
Union: $\small \forall A \ \exists x \ \forall y \ (y \in x \leftrightarrow \ \exists z \in A (y \in z))$
Power:$\small \forall A \exists x \ \forall y \ (y \in x \leftrightarrow \ \exists \forall z \in y (z \in A))$
Regularity: $\small \exists x \in A \rightarrow \exists x \in A \ \forall y \in A (y \not \in x)$
Choice: $\small \forall x \ \exists y \ (Ord(y) \wedge x \ is \ equinumerous \ to \ y)$
where "equinumerous to" stands for existence an injection in either direction between x and y.
"ord" stands for Von Neumann ordinal defined as a transitive set of transitive sets.
Note: the original question was asked with the formula in injective replacement being:
$\small [\forall x,y,z,u (\phi(x,y) \wedge \phi(z,u) \rightarrow (x=z \leftrightarrow y=u)) ] \rightarrow \forall A \exists B \ \forall y \ (y \in B \leftrightarrow \exists x \in A (\phi(x,y))$
However, I've corrected it to the one above, since that was my original primary intention.