Where is the equivalence between $x = y$ and $y = x$ defined?

Question

I have been studying the (very elementary) proof of the theorem that the product of two negative real numbers is a positive real numbers. Now I can follow each step in the proof and see how each step uses the axioms of real numbers numbers "under" the operations addition and multiplication (amazing to me the detail needed). Now, in some steps of the proof, the axioms applied are "reversed", or at least that's how I am reading them. E.g. consider $x·0 = 0$, but in the proof the "reverse" property is used, e.g., $0 = x·0$. So my question (finally) is: if $x = y$ is an axiom, then where is the "property" $y = x$ "defined"? Hopefully that question is clear.

Answer 1

Usually $=$ is somewhat of a metatheoretical construct. So $a=b$ is taken as the metatheoretical statement "the mathematical objects $a,b$ are the equal, or the same". Thus this symmetry is not really a mathematical axiom, but one of the fundamental metatheoretical axioms you need to do maths.

This is something that exceeds any mathematical model, be it some logical model, some set model, a categorial model or whatever. No matter what mathematical base model you have, you will always assume this metatheoretical axiom $a=b$ is equivalent to $b=a$.