"If $b = c$ then $a \oplus b = a \oplus c$" with minimal assumptions about objects and foundations I am confused about something that seems to be known as the "substitution property," which I take to be central to mathematical reasoning. Informally:
$$
\text{If } b = c \text{ then } a \oplus b = a \oplus c.
$$
I don't remember ever seeing the above inference defined or proved, which leads to cognitive dissonance when trying to follow algebraic proofs that employ it. Where does it come from? If it depends on choice of foundations, what are the alternatives? Do I need to take courses in Mathematical Logic and Type Theory to understand what is going on here?
To capture the way that I currently reason about things, I have restated the problem below. I think that my confusion would be resolved if I could prove the following proposition:

Let $X$ be a mathematical structure of unspecified foundations.
For any symbol $a$, "$a$ is an $X$" is either true or false.
We will write "$a, b, \ldots$ are $X$" to mean $a$ is an $X$ and $b$ is an $X$ and $\ldots$
Let $\oplus_X$ denote a symbol that combines any two symbols $a$, $b$ such that:

*

*if $a$, $b$ are $X$ then $a \oplus_X b$ is an $X$.

Let $=_X$ denote a symbol that combines any two symbols $a, b$ such that:

*

*if $a, b$ are $X$ then $a =_X b$ is either true or false

*if $a$ is an $X$ then $a =_X a$

*if $a, b$ are $X$ then (if $a =_X b$ then $b =_X a$)

*if $a, b, c$ are $X$ then (if $a =_X b$ and $b =_X c$ then $a =_X c$)

Proposition:
If $a, b, c$ are $X$ and $b =_X c$ then
$a \oplus_X b =_X a \oplus_X c$
[Note: fixed serious typo, had written If $a, b, c$ are $X$ and $b =_X c$ then $a \oplus_X b = a \oplus_X c$]

Is the proposition provable from the given definitions? If not, what are the missing ingredients? Are they a property of the chosen logic? Or of the choice of foundations? (e.g. Set theory, Type theory) If so, how? Or does the proposition always depend on the structure X? i.e. should the proposition always be proved?
My reading so far has lead me to the following unresolved ideas:

*

*In high-school algebra, it would appear that the "substitution property" is taken as axomatic. Is this also the case in abstract Algebra? or in mathematical reasoning more generally?


*Often, $X$ is defined as a Set with some additional structure (e.g. a Group), so perhaps some basic property of Sets is assumed?


*In contexts involving equivalence classes, we must prove that the "operation" $\oplus_X$ is "well-defined". (One of my teachers used to say that really we are asking whether $\oplus_X$ is "defined" at all!) Perhaps this means that the "substitution property" is an implied property, or part of the definition of an "operation"? Although I found no such information in the definition of operation[1].


*An unanswered question[2] mentions the "Axiom of Substitution" but I don't remember seeing such an axiom and I could not find a definition of it.
My background: I am a student of mathematics at the level of a not strong mid-to-upper level undergraduate. I also have an informal background in computer programming. I have not studied mathematical foundations or mathematical logic. I read Halmos' Naive Set Theory a long time ago, I have not read Bourbaki (but I can if you think it will help), I have heard of HoTT, I have seen a definition of natural deduction, and I know that sometimes "=" is used to mean canonical isomorphism. I would be comfortable if your answer involved these and other related concepts.
[1] https://en.wikipedia.org/wiki/Operation_(mathematics)#Definition
[2] Question about the axioms of equality, particularly about the axiom of substitution
 A: 
Is the proposition provable from the given definitions?

Clearly not. If we’re working in set theory, all these axioms require is that $=_X$ is a (decidable) equivalence relation on $X$. There is no reason to think that an operation should respect all possible equivalence relations.
In first-order logic with equality, we have the following rule. We can derive $P(y)$ from the premises $x = y$ and $P(x)$. This is a basic rule/axiom of first-order logic with equality.
We can also always derive $x = x$. This is the reflexive property of equality.
In particular, let $P(x)$ be the proposition $a \oplus b = a \oplus x$. Then $P(b)$ is an instance of the reflexive property of equality, so we know $P(b)$. If we then assume $b = c$, it follows from the substitution property that $P(c)$ also holds. That is, $a \oplus b = a \oplus c$. So we have proved that if $b = c$, then $a \oplus b = a \oplus c$.
Type theories vary somewhat in their treatment of equality, but they usually have a version of the substitution property and reflexive property as axioms. Thus, the proof in type theory should look similar to the proof in first-order logic.
