SUBSTITUTION: Let $\mathbf{F}$ be any algebraic structure. For each $a$, $b\in \mathbf{F}$ if $a=b$ then $a$ can be replaced with $b$ in any mathematical statement involving $a$ and the statement will preserve it's truth value.
In all rigorous mathematical books I have read, the "axiom" of substitution for equality is assumed to be true almost a priori to even listing axioms for equality. Is this because substitution is so fundamental that it is assumed to be understood? Often a book will say that $=$ is an equivalence relation on all numbers so that it is reflexive, symmetric and transitive. This is often treated as the "axioms" for equality. The only issue is the text will often proceed to use some sort of "substitution" rule as well.
For example, in Baby Rudin, the following is the proof for the fact that if $x+y=z+y$ then $x=z$ for each $x$, $y$, $z\in \mathbf{F}.$ $$x=x+0=x+(y+(-y))=(x+y)+(-y)=(z+y)+(-y)=z+(y+(-y))=z+0=z.$$ As I see it, the second, fourth and sixth equal sign above uses an elusive, "substitution like" property that I do not think has been addressed in the book. Why is that?
Also, by my understanding, one only needs "reflexivity" and "substitution" to prove that symmetry and transitivity hold. See here. Is it possible to "prove" a substitution property from the three properties of an equivalence relation?
If I were to teach mathematics and give some sort of set of "axioms for equality" could I say that one only needs TWO: first, the reflexive property and second, the substitution property? Prove symmetry and transitivity as homework?
Substitution can refer to multiple things. One of which is substituting equal things as you've described here, another is substituting an expression for the value of a variable, which is not fundamentally about equality. I'll mostly talk about the equality-flavored concept.
Substitution can be taken as a rule of inference (not an axiom because it has a premise and a conclusion instead of just being a conclusion), but you can also prove that it is semantically valid.
Let's take a detour into the semantics of first-order logic.
In its modern form, $=$ denotes real, bona fide sameness, and it's an inherent part of your logic, not part of the theory of real numbers or whatever theory we're looking at. $2+2 = 4$ isn't expressing a relationship between two distinct objects, it's saying that they are the same object. This gets a little more complicated when you think about variables like $x = 7$, but we have to remember that expressions or formulas containing variables always exist in some context and that context is what supplies them with a concrete interpretation. $x = 7$ is not expressing a relationship between some object that is $x$ the variable and the number $7$.
So that's the justification for the substitution rule semantically. Two equal things are really one thing and that's why expressions denoting them can be swapped around.
This isn't the only way of doing things however.
You can treat $=$ as an equivalence relation with some additional rules in your semantics rather than making it "true sameness". Although, again, this is not the modern approach.
Being an equivalence relation is not enough. For the substitution property to hold, $=$ also needs to be a congruence with respect to all function and relation symbols, i.e.
$$ x_1 = y_1 \land \cdots x_n = y_n \to f(x_1\cdots x_n) = f(y_1 \cdots y_n) \\ \text{must hold for all function symbols $f$} $$
$$ x_1 = y_1 \land \cdots x_n = y_n \to (R(x_1\cdots x_n) \leftrightarrow R(y_1\cdots y_n)) \\ \text{must hold for all relation symbols $R$} $$
The effect of those rules is two make two things $a$ and $b$ where $a = b$ holds indistinguishable. Even if, at a semantic level, $a$ and $b$ are different, no question we can ask using the (first-order) language of real numbers can distinguish them.
We can talk about substitution in deductive systems (i.e. proof calculi), but most of the time that's about instantiating variables rather than swapping around equal things.
I can think of one system that has an equality-flavored rule like this.
Take equational logic.
The substitution rule allows us to infer $P[x := E]$ from $P$. This means inferring $1 = --1$ from $x = --x$. This is not fundamentally related to equality.
The Leibniz rule, however, allows us to infer $E[x:=P] = E[x:=Q]$ given $P = Q$. This is about equality. This allows us to infer $1 + 3 = 1 + 4$ from $3 = 4$. $1 + 3 = 1 + 4$ is not correct, but the conclusion does follow from the premise.
An version of this rule that's not tied to any specific deductive system is also being used to conclude that $(x + y) - y = (z + y) -y$ in your example from the hypothesis $x + y = z + y$.