Theorem resubid1

Description: Real number version of subid1 without ax-mulcom . (Contributed by SN, 23-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		readdlid	$$⊢A\in ℝ\to 0+A=A$$
2		id	$$⊢A\in ℝ\to A\in ℝ$$
3		elre0re	$$⊢A\in ℝ\to 0\in ℝ$$
4	2 3 2	resubaddd	$$⊢A\in ℝ\to \left(A{-}_{ℝ}0=A\leftrightarrow 0+A=A\right)$$
5	1 4	mpbird	$$⊢A\in ℝ\to A{-}_{ℝ}0=A$$