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.