Axiom of extensionality in ZF - pointless?

It is true that different authors have suggested that extensionality feels closer to a logical axiom than something else, and can be seen as defining equality in terms of membership. The question is then whether this is indeed innocuous.

This was considered seriously by Dana Scott, in

Dana S. Scott. More on the axiom of extensionality, in Essays on the foundations of mathematics, dedicated to Prof. A. H. Fraenkel on his 70th birthday, Magnes Press, The Hebrew University, Jerusalem, 1961, pp. 115–131. MR0163838 (29 #1137).

Scott considers Zermelo's set theory $\mathsf{Z}$, the standard system of Zermelo-Fraenkel $\mathsf{ZF}$, and their variants $\mathsf{Z}^{\ne}$ and $\mathsf{ZF}^{\ne}$ where extensionality is not assumed. Recall that in $\mathsf{Z}$ we do not assume replacement. (The precise formulation of these theories has some minor technical caveats, see section 1 of the paper.)

Scott shows:

1. There is a relative interpretation of $\mathsf{Z}$ inside $\mathsf{Z}^{\ne}$.

2. There is a relative interpretation of $\mathsf{ZF}^{\ne}$ inside $\mathsf{Z}$.

The significance of these results is that of course there is no such interpretation of $\mathsf{ZF}$ within $\mathsf{Z}$, since in fact $\mathsf{ZF}$ proves the consistency of $\mathsf{Z}$. On the other hand, 1 and 2 show that the theories $\mathsf{Z}$, $\mathsf{Z}^{\ne}$, and $\mathsf{ZF}^{\ne}$ are equiconsistent. This proves that the removal of extensionality actually significantly weakens the reach of set theory, and leaves us with a theory of considerably lower consistency strength.

A different issue is whether this would affect mathematical practice, since most of "classical" mathematics does not require replacement anyway (so it can be carried out in $\mathsf{Z}$ and therefore in $\mathsf{Z}^{\ne}$). However, I feel this argument no longer holds water (if it ever did), since big portions of "modern" mathematics do use and need replacement routinely (and so the weaknesses of $\mathsf{ZF}^{\ne}$ with respect to $\mathsf{ZF}$ become now matters of serious concern).

We want to connect the two basic relation symbols, $\in$ and $=$. The axiom of extensionality tells us that if two sets are distinct then there is some witness of this in the universe. Consider the very contrived example $\{\varnothing,\{a\}\}$, with the usual $\in$. The element $a$ is not in the universe of this example, so it cannot internally discern between $\varnothing$ and $\{a\}$.

Suppose the set $S$ contains the element $a$ and no other elements.

Suppose the set $T$ contains the element $a$ and no other elements.

Should these sets be equal? If you think so, then you'll have to use extensionality to argue as such: it is the only axiom of ZFC that allows you to infer that two sets are equal.