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.