How to prove that $((x+a) = (y+a)) \to (x = y)$ I'm trying to prove the above, using only the axioms of the real numbers and first order logic.  That is, the field axioms for real numbers plus the following:


*

*$(\forall x,y \in \mathbb R)((x \geq y \wedge y \geq x) \rightarrow x = y)$

*$(\forall x,y \in \mathbb R)((x \geq y \wedge y \geq z) \rightarrow x \geq z)$

*$(\forall x,y \in \mathbb R)(x \geq y \vee y \geq x)$

*$(\forall x,y \in \mathbb R)(x \geq y \rightarrow x + z \geq y + z)$

*$(\forall x,y \in \mathbb R)((x \geq 0 \wedge y \geq 0) \rightarrow xy \geq 0)$


I'm satisfied that $(x = y)\to ((x+a) = (y+a))$ and already have a proof of this, but am not sure how to prove the reverse and hence prove $(x = y) \leftrightarrow ((x+a) = (y+a))$
Would it be a valid proof if I just did the following?
$(x + a) = (y + a) \to (x + a) + c = (y + a) + c$  (from theorem above)
Let $c = -a$, then 
$(x + a) = (y + a) \to (x + a) + (-a) = (y + a) + (-a)$
$(x + a) = (y + a) \to x + (a + (-a)) = (y + (a + (-a))$ (Associative law)
$(x + a) = (y + a) \to x + 0 = y + 0$ (Inverse law)
$(x + a) = (y + a) \to x = y$ (Identity law)
This doesn't feel right to me, because we're making an assumption that c is some specific value, so I feel this proof is bogus.  Can anyone point me in the right direction?
 A: Your proof is correct. The rule which states that you can add the $c$ on both sides of the quality states that this holds for any $c$, so in particular for $-a$. Note that this is in fact just the first of the two rules you proved, namely $x = y \to (x + a = y + a)$. Except now you use $-a$ instead of $a$.
A: The proof is correct, a bit too long but essentially right.
Notice that you only need the group axioms to prove the statement because $\Bbb R$ is an ordered field and consequently an abelian group respect to the sum.
Axioms for any group $(G,\oplus)$


*

*$\forall a,b\in G: a\oplus b=c\implies c\in G$, i.e. $\oplus$ is an operation in $G$.

*$\forall a,b,c\in G: (a\oplus b)\oplus c=a\oplus(b\oplus c)$, i.e. $\oplus$ is an associative operation.

*$\exists e\in G: a \oplus e=e \oplus a=a,\forall a\in G$, i.e. the $\oplus$ operation have an identity element.

*$\forall a\in G,\exists b\in G: a\oplus b=e$, i.e. every element of $G$ have an inverse respect to the $\oplus$ operation.
Then $(\Bbb R,+)$ is an abelian group (a group where $a+b=b+a$), and using the above axioms we have
$$(x+a)=(y+a)\to (x+a)+(-a)=(y+a)+(-a)\to x+0=y+0\to x=y$$
Note: the valid pass from $(x+a)=(y+a)$ to $(x+a)+c=(y+a)+c$ is a consequence of an operation being a function, so you can justify it directly from the group axioms without any relation to some axiom of an ordered field.
