From [$\sf L-S$][1] theorems we can have an external bijection $j$ from a set to its powerset. Obviously, $j$ cannot be fully internalized (used in all instances of Replacement). However, partial internalization is possible. The question here is about if $j$ can be partially internalized in the particular manner described below:

$\exists  \alpha: \text{ limit} (\alpha) \land j: V_\alpha \to V_{\alpha +1} \land j \text{ is a bijection }$

$ \forall A  \ \exists B: B=\{\{j(m),j(n)\} \mid \{n,m\} \in A\}$

$ \forall A  \ \exists B: B=\{\{n,m\} \mid  \{j(m),j(n)\} \in A\}$

In the other words, is it consistent to add to the language of $\sf ZF$ a partial function symbol $j$, and add [to axioms of $\sf ZF$] the above three sentences as axioms? Provided, of course, that Replacement doesn't use $j$.


  [1]: https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_theorem