Add a primitive partial unary function symbol $F$ to the first order language of set theory.
Working in Zermelo (Separation restricted to the language of set theory), add the following axioms:
$F$ function: $\exists X ( F: \mathcal P(X) \longrightarrow X, F \text { is injective} )$
Forward copying:$ \forall A \exists B: B = \{ \{ F(n)| n \in m \}| m \in A \} $
Backward copying: $ \forall A \exists B: B = \{ \{ n| F(n) \in m \}| m \in A \} $
Now if $F$ happens to be an isomorphism on $\in$, then $F$ cannot be bijective! Since the parity of the set of all ordinals in $\mathcal P(X)$ is different from that in $X$. Hence the following questions:
Is there an example of $F$ that is not an isomorphism on $\in$?
If so, then is it the case that the qualifications of $F$ in the above system are still enough as to forbid $F$ from being a bijection?
The rationale beyond the above question is that if there is no clear argument against $F$ being bijective, then this might entail opening the door for a possible proof of $\sf Con(NF)$, as $F$ being bijective would easily interpret a finite axiomatization of $\sf NF$. The interpretation is over $X$ using a new membership relation $\in^F$ defined as: $$ y \in^F x \iff y \in F^{-1}(x)$$