x'=y'→x=y
これは後者関数の単射であることを意味する。
ペアノの公理からこれを除くと、ループを許すことになる（例えばこんなの↓）。
0→1→2→3→1→2→3→1→2→3→…

形式的な話をすれば、体系内で帰納的関数を構成する際などにこの公理を用いる。
もちろん、それ以外の場面でも。

上でも指摘されてるけど、
x=y→x'=y
これ↑は単なる代入可能性を意味する、等号の公理の一部。