To see what I mean, this is how Kunen puts the matter:
"Intuitively, x=y means that x and y are the same object. This is reflected formally in the fact that the basic properties of equality are logically valid and need not be stated explicitly as axioms of ZFC. For example,
|- (x=y -> Az(zex <-> zey))
whereas the converse is not logically valid, [...]"
If you look this up, you will feel that I have excluded something important. But, the rest of the statement involves a theorem based on extensionality and pairing.
Jech begins with the statement of extensionality followed by the disclaimer:
"If X and Y have the same elements then X=Y:
Au(ueX <-> ueY) -> X=Y
The converse, namely, if X=Y then ueX <-> ueY, is an axiom of predicate logic."
So, there are reasons why I took such care in the construction.
At the end, the object had been to topologize the structures so that the sense of what you have written above was explicitly demonstrated as being essential to the construction of the reals by Dedekind cuts.
Since the explanation of Leibniz' Law in the article cited above is not what Leibniz actually wrote when explaining it, the proper way of introducing a metric structure is found in Kelley's discussion of uniform spaces and his metrization lemma.
Given a "logical" identity, the psuedometric axiom
x=y -> d(x,y)=0
puts a topology onto it.
And, since you are so competent when it comes to topology, go to the back of Steen and Seebach to the section where they discuss non-metrizable topologies:
Tangent Disc Topology (and Bing's flow space variation)
Tangent Disc Subspaces
Moore's Road Space
And, consider Fleissner's example mentioned in the Addendum to that section in the context of