Is the Axiom of Extensionality needed in predicate logic without equality? In predicate logic with equality, defining the Axiom of Extensionality allows us to gain the logical property of substitution. I have seen the axiom formulated as
\begin{equation}
    \forall x: \forall y: \left( \forall u: \left( u \in x \iff u \in y \right) \implies x = y \right)
\end{equation}
where $x=y$ is the pre-existing notion of equality from predicate logic. By defining it in this way, we have the property of substitution; that is, by the axioms of predicate logic,1 we can replace instances of $x$ with $y$ (and vice versa).
On the other hand, in predicate logic without equality, we do not gain the property of substitution by defining the Axiom of Extensionality.2 In this case, the Axiom of Extensionality can be written as
\begin{equation}
    \forall x: \forall y: \left( 
        \forall m: \left( m \in x \iff m \in y \right) \implies 
        \forall u: \left( x \in u \iff y \in u \right)
    \right) .
\end{equation}
This is the way it appears on Wikipedia. It seems like the goal of this formulation is to state that if two sets contain the same elements, they are elements of the same set.
For some arbitrary set $u$, we could define $x = \{u\}$, $y = \{u\}$, and $z = \{x\}$. Then we ask: is $y \in z$? The Axiom of Extensionality tells us that this is true, but we don't need the axiom of extensionality to prove this! We could simply define, without need for the axiom of extensionality, a relation $p = q \;:\Longleftrightarrow\; \forall r: (r \in p \iff r \in q)$.
Then, by the pair set axiom:
\begin{equation}
    \forall a: \forall b: \exists c: \forall d: \left( d \in c \iff d=a \lor d=b \right) \end{equation}
we can choose $a = b = x$ to conclude that:
\begin{align}
    &\exists z: \forall d: \left(d \in z \iff d=x\right) \\
    &\exists z: \forall d: \left(d \in z \iff \forall r: \left(r \in d \iff r \in x\right)\right)
\end{align}
I have used $z$ here to mirror the construction of $z$ from before: a set which contains only $x$ as an element. However, it's very simple to check that both $y \in z$ and $x \in z$ via this construction, and so it seems that the Axiom of Extensionality is not needed.

So... 
Is this line of reasoning correct? If not, what is the purpose of the Axiom of Extensionality in set theory defined under predicate logic without equality?

Similar questions:

*

*Should this "definition" of set equality be an axiom? and Why isn't the axiom of extensionality considered a definition of equality? explain that the Axiom of Extensionality is used in set theory under predicate logic without equality, but do not explain why it is needed.


*Axiom of extensionality in ZF - pointless? claims that the Axiom of Extensionality limits the "reach" of set theory, but does not specifically address the problem w.r.t. set theory under predicate logic without equality.

1 For example, see Introduction to Mathematical Logic, page 74 
2 The property is not defined in the axioms of predicate logic without equality, and so we cannot gain a property which does not exist. 
 A: Your reasoning is correct in that if you define $\{x\}$ in this way, you can show that $y \in z$.
However, consider the set $z’ = \{w \in z \mid \forall k (x \in k \to w \in k\}$. Of course, $z’$ is only defined up to “equality”, and its definition requires separation.
Note that we can conclude $x \in z’$. But concluding that $y \in z’$ amounts to assuming extensionality, which we cannot do.
It’s fairly simple to come up with a model of set theory in which extensionality is false. Let $2 = \{0, 1\}$. Simply take the smallest class $U$ such that for all sets $s \subseteq U$ and all $x \in 2$, we have $(s, x) \in U$. Proving such a class exists requires some cleverness, but it’s not too hard.
Then define $\in_U$ by $w \in_U (s, x)$ iff $w \in s$. You can verify that all axioms except extensionality hold in $U$. This is an instructive model for understanding why extensionality fails; play around with it a bit, and can find an $x, y, z’$ as described above where $x$ and $y$ have the same elements and $x \in z’$ but $y \notin z’$.
