This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ A + B = B

Proof

Step Hyp Ref Expression
1 readdsub ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → A + B - ℝ A = A - ℝ A + B
2 1 3anidm13 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B - ℝ A = A - ℝ A + B
3 repncan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B - ℝ A = B
4 2 3 eqtr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ A + B = B