Terence Tao, Analysis I, 3e,
(...) How equality is defined depends on the class T of objects under consideration, and to some extent is just a matter of definition. However, for the purposes of logic we require that equality obeys the following four axioms of equality:
- (Reflexive axiom) (...)
- (Symmetry axiom) (...)
- (Transitive axiom) (...)
- (Substitution axiom). Given any two objects $x$ and $y$ of the same type, if $x = y$, then $f(x) = f(y)$ for all functions or operations $f$.
Concerning the substitution axiom, I keep wondering if there is really no way one could prove that
$$ x = y \Rightarrow x + z = y + z, $$
where $x, y, z$ are natural numbers?