Theorem resubid1

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

	Ref	Expression
Assertion	resubid1	|- ( A e. RR -> ( A -R 0 ) = A )

Proof

Step	Hyp	Ref	Expression
1		readdid2	|- ( A e. RR -> ( 0 + A ) = A )
2		id	|- ( A e. RR -> A e. RR )
3		elre0re	|- ( A e. RR -> 0 e. RR )
4	2 3 2	resubaddd	|- ( A e. RR -> ( ( A -R 0 ) = A <-> ( 0 + A ) = A ) )
5	1 4	mpbird	|- ( A e. RR -> ( A -R 0 ) = A )