Axiom of extensionality - why can't we replace $\Rightarrow$ with $\iff$? The axiom of extensionality says that 
$$(\forall(x,y))\big(\forall(z)(z\in x\iff z\in y)\Rightarrow x=y\big)$$ 
Does it not work the other way around?  
$$ (x=y)\Rightarrow\forall z(z\in x\iff z\in y) $$
If two sets are equal and $z$ is in one of them, then - by definiton - it has to be in the other one. 
If it is not true, could you show a counter-example?
 A: "The other way around" is true and no axiom is needed for that. 
If $x,y$ are somehow labels of the same set ($x=y$) then automatically every $z\in x$ will satisfy $z\in y$ (and vice versa).
The axiom of extensionality is the statement that the opposite direction of this is also true. That does not speak for itself so really needs an axiom.

edit: 
We have sets and we have a relation on them denoted by $\in$. 
Then a new relation can be induced as follows:$$a\subseteq b\iff \forall x[x\in a\implies x\in b]$$
This relation $\subseteq$ is evidently transitive and reflexive, which means that we are dealing with a preorder. Now the axiom of extensionality is actually the statement that relation $\subseteq$ is also antisymmetric. That means that $\subseteq$ can be looked at as a partial order.
Caution: I used the term "relation" in my edit, but not in a formal way. 
We are not dealing with  sets $\{\langle a,b\rangle\mid a\in b\}$ or $\{\langle a,b\rangle\mid a\subseteq b\}$.
A: The converse of extensionality is a result of the axioms
of a first order logic with equality.  An alternative to
embedding ZF into a first order logic with equality is to
embed it into a first order logic and use the axiom of
extensionality as a definition of equality.  Then the
"converse" would be an iteration of the definition.
