Postulate for elimination?

In proving that the elimination method of adding linear equations works, does one need to show that it is equivalent to substitution?

Using the transitive or substitution property to solve a system of equations is on solid ground because those can be taken as postulates. However there is no elimination postulate, is there?

Also if you don't write y=x+4 and y=2x like so but instead as

f(x)=x+4 and g(x)=2x

then if you add and get

f(x)+g(x)=3x+4

and then write it as

2f(x)=3x+4

then we are implicitly setting f(x)=g(x) right? I guess by using the same letter, y, for each line is just a shortcut for not having to explain what is really going on. Prof. Jerison mentions this "sloppiness" in the first lecture of MIT's OCW Calculus.