Define: $x=^*y \iff \forall m \ (m \in x \iff m \in y)$,
i.e. $=^*$ is co-extensionality relation.
Define: $ Set(x) \iff \forall y,z \ (y \in x \wedge z=^*y \implies z \in x)$
i.e. a set is a union of 'equivalence classes under co-extensionality'
Define: $ x \in^* y \iff Set(y) \wedge x \in y $
Can $\text{ZF-Extensionality}$ (with the axiom schema of Replacement formalized in a conventional manner) prove the following scheme?
If $\phi(x)$ is a formula that only uses the symbols $``=^*",\ ``\in^*"$ as predicate symbols, in which the symbol $``x"$ occurs free and never occurs as bound, and in which the symbol $``y"$ does not occur, and if $\phi(y)$ is the formula obtained from $\phi(x)$ by merely replacing all occurrences of the symbol $``x"$ by the symbol $``y"$ then all closures of the following are theorems:
$\forall x,y \ (\phi(x) \wedge y=^*x \implies \phi(y))$
I personally think that the answer is to the positive since atomic formulas $x \in^* y,\ x=^*y$ are clearly preserved under co-extensionality, and their negation, conjunction and disjunction are clearly so as well, and it appears to me that adding quantifiers to any formula that satisfy the above property will also satisfy it.
I'm asking this question in relevance to my latter question that I've asked at:
Equivalents of Replacement under removal of Extensionality?
I think if the above is true, then I think that the last version of $\text{ZF-Extensionality}$ mentioned in that link, would interpret $\text{ZFA}$ over its domain by using relations $=^*,\ \in^*$, and $\text{ZFA}$ clearly interprets $\text{ZF}$.
