Is the injectivity scheme present in the below axiomatic exposition of a first-order set theory provable in $\text{ZF}$?


**Extensionality:** $\forall A,B \ [\forall x \ (x \in A \leftrightarrow x \in B) \to A=B]$


**Empty:** $\exists O \ \forall x \ (x \not \in O)$


**Union:** $\forall A \ \exists U \ \forall x \ (x \in U \leftrightarrow \exists y \in A \ (x \in y))$


**Intersection:** $\forall A \ \exists I \ \forall x (x \in I \leftrightarrow \exists y \in A (x \in y) \ \wedge \forall y \in A (x \in y))$


**Injectivity:** If $\phi(x,A)$ is a formula in which the symbols $``x", ``A"$ occur free and only free and in which the symbol $``B"$ doesn't occur, and $\phi(x,B)$ is the formula obtained from $\phi(x,A)$ by merely replacing all occurrences of the symbol $``A"$ by the symbol $``B"$, then all closures of:


$ \forall wf(A) \ [\forall x \ (\phi(x,A) \to wf(x))] \wedge \\ \forall A,B \ \big{(} \forall x (\phi(x,A) \leftrightarrow \phi(x,B) ) \to A=B\big{)} \\ \to \forall A \ \exists B \ \forall x \ \big{(}x \in B \leftrightarrow \phi(x,A) \big{)} $


are axioms.


where $wf$ stands for the predicate ***"is well founded"***, defined as:


$$ wf(x) \iff \not \exists c \ ( x \in c \wedge \forall m \in c \ (\exists n (n \in m \wedge n \in c))) $$


**Infinity:** $\exists N \ [\emptyset \in N \wedge \ \forall x \in N (x \cup \{x\} \in N)]$


The point of this question is that the above theory (if consistent) then it proves all axioms of $\text{ZF-Foundation}$, and so it interprets the whole of $\text{ZFC}$, Injectivity would prove injective replacement of elements of well-founded sets by well-founded sets, Pairing trivially follow, and Separation follows from having intersection with injective replacement, of course Power trivially follows from Injectivity. However, I couldn't manage to prove the injectivity schema in $\text{ZF-Foundation}$. Which raises suspicion about its consistency with the other axioms.


There is another related aside question, should this prove to be consistent relative to $\text{ZF}$, what should we regard the non-well founded objects that must exist in this theory? Are they sets? if they are not sets? then why did they play a rule in the construction of well-founded set? In a more general sense: If it proves very useful to have non-well founded objects to construct well-founded sets, then how are we to consider those non-well founded objects, would they be considered as "sets"? or still as another kind of objects?


**Afternote:** The Injectivity axiom schema is inconsistent. Andreas Blass has shown that we can have a set of all ordinals $\geq 2$ and singletons of elements a set $A$, for any arbitrary set $A$, now take $A=\emptyset$, and we get the set of all ordinals $\geq 2$, take its union and then we can get the set of all ordinals, which is inconsistent. I don't think this can be easily fixed.



Is the following injectivity schema provable in ZF-foundation?
No, some instances of the injectivity scheme are refutable in ZF. For example, let $\phi(x,A)$ say "either $x$ is an ordinal $\geq2$ or $x=\{y\}$ for some $y\in A$. (To verify the second hypothesis of injectivity for this $\phi$, use that an ordinal $\geq2$ is never a singleton.)


