Theorem resubidaddlid

Description: Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023)

	Ref	Expression
Assertion	resubidaddlid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A{-}_{ℝ}A\right)+B=B$$

Proof

Step	Hyp	Ref	Expression
1		readdsub	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\in ℝ\right)\to \left(A+B\right){-}_{ℝ}A=\left(A{-}_{ℝ}A\right)+B$$
2	1	3anidm13	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A+B\right){-}_{ℝ}A=\left(A{-}_{ℝ}A\right)+B$$
3		repncan2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A+B\right){-}_{ℝ}A=B$$
4	2 3	eqtr3d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A{-}_{ℝ}A\right)+B=B$$