What is the name of the rule that allows us to infer the truth of an equation from the truth of another equation?

Question

I am wondering if there is a particular named rule or principle in mathematics/formal logic (that can be listed as justification in a formal proof) that allows one to conclude the truth of an equation if we know that this equation is simply a modification of another equation (assumed to be true) where that modification was an operation applied to both sides of that other equation. For example, the principle that we can use to infer that x + 1 = y + 1 if we already know that x = y.

Answer 1

It depends on the logical framework within which you are working. While there are many "laws of reasoning", what's actually allowed is specified by a given proof system of which there are many – even for the same logic and then there are many logics.

Nevertheless, one of the simplest and most common ways of doing this within first-order logic is via the following rule (or some variant presentation of it): $$\dfrac{x=y\qquad P(x)}{P(y)}$$

The old-timey "law of reason" name for this (or rather the derivable statement that $x=y\to P(x)\leftrightarrow P(y)$ for all $P$) is the "indiscernibility of identicals".¹ A more modern name might be "substitutivity".² From the perspective of natural deduction, this can be viewed as an elimination rule for $=$ and thus may be called "$=$ elimination". Combined with reflexivity, this allows you to prove all the properties you'd expect of equality. For example, you can show that it is an equivalence relation. For your particular case, we can choose $P(z)$ to be $x+1=z+1$, then $P(x)$ holds via reflexivity and thus, given $x=y$, we can derive $P(y)$ which is $x+1=y+1$.

It is extremely uncommon for mathematicians to actually explicitly state this as a proof step.

¹ That page also talks about the identity of indiscernibles also known as Leibniz's law. This is the converse.

² The analogue to this in constructive type theory has the super clear name of $J$.