In Peano's Axioms are the uniqueness of the successor and the property $x^{\prime}=y^{\prime}\implies{x=y}$ redundant?
This seems obvious to me, but I may be missing something. In the various forms of the axioms used as the basis of natural number arithmetic that I have seen, the successor of a number is, in the axiom stating its existence, defined to be a unique number. That appears to require that $x^{\prime}=y^{\prime}\implies{x=y}$. So stating this result as an additional axiom is redundant.
On the other hand, $x^{\prime}=y^{\prime}\implies{x=y}$ seems insufficient to show that the successor of a number is unique.
From my perspective, such a redundancy is not particularly offensive if it aids in the applicability of the set of axioms. But such a feature should be explained, perhaps in a footnote. Since I have seen no such footnote, I am motivated to ask if others agree with my understanding.