Theorem resubidaddlid

Description: Any real number subtracted from itself forms a left additive identity. (Contributed by Steven Nguyen, 8-Jan-2023)

	Ref	Expression
Assertion	resubidaddlid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐴 ) + 𝐵 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		readdsub	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = ( ( 𝐴 −ℝ 𝐴 ) + 𝐵 ) )
2	1	3anidm13	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = ( ( 𝐴 −ℝ 𝐴 ) + 𝐵 ) )
3		repncan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = 𝐵 )
4	2 3	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐴 ) + 𝐵 ) = 𝐵 )