In Tao's analysis volume 1, I am introduced to this thing called the axiom of substitution. While constructing real numbers from rationals, he defined reals to be formal limits of Cauchy sequences of rationals. He said $\lim a_n=\lim b_n$ iff $(a_n)$ and $(b_n)$ are equivalent sequences. Then he defines addition of reals as - $\lim a_n + \lim b_n=\lim(a_n+b_n)$. Then he verifies that the axiom of substitution is not violated i.e. if $x=x'$ then $x+y=x'+y$. (I like to state this as "addition is well-defined").
My question : It seems that the axiom of substitution is a rather fundamental one that one needs to verify whenever a binary operation (such as addition) is introduced. However, not once in our course on group theory did we verify this axiom when we defined a binary operation on a set (and tried to show it forms a group). Shouldn't it be the first step?
In this definition, real numbers are defined as equivalence classes of Cauchy sequences under an equivalence relation $\sim$, and then addition of real numbers is defined by first defining it on Cauchy sequences and then showing that it respects the equivalence relation (this is what "well-defined" means), so that it "descends" to equivalence classes.
If you're in a situation where you also need to define an operation on a set of equivalence classes $X/\sim$ by first defining it on $X$ and then showing that it respects $\sim$, then you also need to do this. But you don't always need to do this, because you aren't always working with equivalence classes. For example, the natural numbers $\mathbb{N}$ aren't defined in this way, and addition of natural numbers is formally defined in a completely different way, via induction.