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?](https://mathoverflow.net/questions/289943/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}$. 



Is this kind of predication preserved under co-extensionality?
This is similar to the main idea behind the Friedman analysis of ZF without extensionality. Without extensionality, one defines a notion of equivalence on sets, of having the same members, but then successively refines the equivalence to having equivalent members, and in this way arrives at a model of set theory. 


See this question: [Is there any research on ZF without extensionality?](https://mathoverflow.net/q/168287/1946) 


My view is that this process exhibits some affinities with the univalence axiom in HoTT.


