In "Analysis with an introduction to proof" (5th ed.) by Steven R. Lay, the existence of a set $\mathbb{R}$, and two binary operations $+$ and $\cdot$, satisfying 15 axioms is assumed.
The first axiom is:
For all $x,y\in \mathbb{R}, \, x+y\in \mathbb{R}$ and if $x=w$ and $y=z$, then $x+y=w+z$
My question: Isn't everything after the first "and" just the substitution property of equality, or am I missing something?
Yes, you are right. Non-logic texts often fail to distinguish between specific axioms and the basic logical framework that those axioms live in (of which the substitution property is a rule).
(For that matter, the part before the "and" is also usually included in the basic set-up of first-order logic, but is less fundamental - allowing partial functions is a much tamer modification than allowing failures of substitution.)
It's not clear to me, incidentally, whether this is pedagogically good or bad in general. On the one hand I do find the distinction between logical framework and specific axioms to be very clarifying; on the other hand, this might reflect my logician's bias, and it may be better for most students to avoid bringing this up - see e.g. the discussion here.
To be more precise, this is essentially a tautology of many-sorted FOL where $ℝ$ is a sort and $+$ is a function-symbol with signature $ℝ^2→ℝ$, that can be proven via 2 applications of the =elim rule. (See here for a complete set of rules for many-sorted FOL.)
Some people might say that we can instead use one-sorted FOL and treat "$∈$" as a relation-symbol (i.e. 2-input predicate-symbol), and treat "$∀x,y{∈}ℝ\ ( \ x+y∈ℝ \ )$" as short-hand for "$∀x,y\ ( \ x∈ℝ ∧ y∈ℝ ⇒ x+y∈ℝ \ )$". This is technically possible, and is how one can show that many-sorted FOL can be translated into one-sorted FOL. However, in my opinion we actually use many-sorted FOL in practice.
Note that "$∀x,y{∈}ℝ\ ( \ x+y∈ℝ \ )$" is not a tautology in one-sorted FOL, so it is needed as an axiom if you use a foundational system based on one-sorted FOL and wish to write down a list of axioms for $ℝ$. However, if you use many-sorted FOL it becomes a design choice; you can either stipulate the output sort (as I did above) or you can still keep this axiom.
Note also that if you ask for the first-order theory of the real structure $⟨ℝ,0,1,+,·,<⟩$, then "$∀x,y{∈}ℝ\ ( \ x+y∈ℝ \ )$" is not even in the language, and instead you just have that any interpretation with structure $⟨ℝ,0,1,+,·,<⟩$ would map "$x+y$" to a member of $ℝ$, just by definition of "interpretation". But people don't want to talk about interpretation of axioms when teaching real analysis, as we simply want to use the axioms instead of having an intervening interpretation layer. So it makes sense to just write down sentences in the foundational system that capture both the language, of which "$∀x,y{∈}ℝ\ ( \ x+y∈ℝ \ )$" is an example, and the axioms, such as "$∀x,y{∈}ℝ\ ( \ x+y = y+x \ )$" (for axiom "$∀x,y\ ( \ x+y = y+x \ )$").
Furthermore, for real analysis the first-order theory of the reals is insufficient, as we need a second-order axiomatization, which sits squarely in the foundational system. This is one big advantage of using many-sorted FOL (as in my first link), since a second-order axiomatization can be trivially expressed in two-sorted FOL and so expressing it directly in the foundational system allows us to invoke the set-existence axioms of the foundational system.
