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).
The second formula is an axiom of the first order logic with equality, together with the following axioms about equality:
- $x=x$.
- $x=y\rightarrow(\varphi\leftrightarrow\psi)$, where and $y$ is free for $x$ in $\varphi$ and $\psi$ is replacing some free variable $x$ by $y$ in $\varphi$.
Unlike Extensionality, which is a proper axiom, these equality axioms are valid in every normal models, hence they deserve the name "logical axioms".
Best Answer
The Axiom of Extensionality cannot be replaced by the statement that two sets are equal if they are contained by the same sets (this latter principle is a form of Leibniz's law, and I will refer to it by that name).
First, let me prove that, unlike Extensionality, $\forall A,B. (\forall x. A \in x \leftrightarrow B \in x) \rightarrow B = A$ follows from the other axioms of set theory, without invoking either Extensionality or Leibniz's law in the proof.
Take any two sets $A,B$, and assume that $\forall x. A \in x \leftrightarrow B \in x$. Define the set $\overline{A} = \{ y \in \mathcal{P}(A) \:|\: y = A \}$ using the Powerset axiom and the Separation schema. Clearly $A \in \overline{A}$, hence by our assumption $B \in \overline{A}$ as well. But by the defining property of $\overline{A}$, the following holds: $\forall y. y \in \overline{A} \leftrightarrow y \in \mathcal{P}(A) \wedge y = A$. In particular, since $B \in \overline{A}$, we can conclude $B = A$.
This proves Leibniz's law in set theory, and since the proof never invokes Extensionality, this implication holds even in set theory without Extensionality.
So all that remains to be shown is that the axiom of Extensionality is not a redudant axiom, i.e. that Extensionality, unlike Leibniz's law, does not follow from the other axioms of set theory. So we have successfully reduced your question to a previous Math.SE question.