ZF Extensionality axiom To familiarize myself with axiomatic set theory, I am reading Kenneth Kunen's The Foundations of Mathematics that presents ZF set theory. I haven't gotten really far since I am stuck at the axiom of Extensionality, stated as follows: $$\forall x,y \; [\forall z(z \in x \leftrightarrow z \in y) \rightarrow x = y]$$ As far as I understood it, the purpose of this axiom is to state that every two sets that have exactly the same members are the same set. In terms of the above formula, when antecedent is true, the consequent needs to be true. What confuses me here is the case when the antecedent is false. Then, the consequent can be false or true, i.e., we can't say much about the consequent. But, don't we really want to say that in that case those two sets are not equal? More precisely, shouldn't we use equivalence instead of implication? If not, what is the reason?

The reason the converse is not part of the axiom is that it already follows from the axioms of first-order logic: $x = y \implies (\varphi(x) \iff \varphi(y))$ for any formula $\varphi$. This is known as the substitution property of equality.