Theorem resubid1

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

	Ref	Expression
Assertion	resubid1	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 −ℝ 0 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		readdid2	⊢ ( 𝐴 ∈ ℝ → ( 0 + 𝐴 ) = 𝐴 )
2		id	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
3		elre0re	⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
4	2 3 2	resubaddd	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 −ℝ 0 ) = 𝐴 ↔ ( 0 + 𝐴 ) = 𝐴 ) )
5	1 4	mpbird	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 −ℝ 0 ) = 𝐴 )