Theorem resubid

Description: Subtraction of a real number from itself (compare subid ). (Contributed by SN, 23-Jan-2024)

	Ref	Expression
Assertion	resubid	$$⊢A\in ℝ\to A{-}_{ℝ}A=0$$

Proof

Step	Hyp	Ref	Expression
1		re0m0e0	$$⊢0{-}_{ℝ}0=0$$
2	1	oveq2i	$$⊢A\left(0{-}_{ℝ}0\right)=A\cdot 0$$
3		sn-00idlem1	$$⊢A\in ℝ\to A\left(0{-}_{ℝ}0\right)=A{-}_{ℝ}A$$
4		remul01	$$⊢A\in ℝ\to A\cdot 0=0$$
5	2 3 4	3eqtr3a	$$⊢A\in ℝ\to A{-}_{ℝ}A=0$$