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.

Equality is often a part of the logical symbols, and if $x=y$ then for every relation $R$, and every $z$ we have $R(x,z)\leftrightarrow R(y,z)$ and $R(z,y)\leftrightarrow R(z,x)$.

In particular $\in$ is such relation.

In older texts, you can sometimes find that people don't assume that $=$ is part of the language and then we simply define $x=y$ as the formula $\forall w(w\in x\leftrightarrow w\in y)$, from which extensionality follows as a theorem. Then the language containing only the binary relation symbol $\in$ (without equality) is called the Language of Set Theory (often abbreviated as LST).