Theorem readdrid

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

	Ref	Expression
Assertion	readdrid	$$⊢A\in ℝ\to A+0=A$$

Proof

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