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

Metamath Proof Explorer

Theorem resubid

Description: Subtraction of a real number from itself (compare subid ). (Contributed by SN, 23-Jan-2024)

		Ref	Expression
	Assertion	resubid	$⊢ A \in ℝ \to A -_{ℝ} A = 0$

Step	Hyp	Ref	Expression
1		re0m0e0	$⊢ 0 -_{ℝ} 0 = 0$
2	1	oveq2i	$⊢ A (0 -_{ℝ} 0) = A \cdot 0$
3		sn-00idlem1	$⊢ A \in ℝ \to A (0 -_{ℝ} 0) = A -_{ℝ} A$
4		remul01	$⊢ A \in ℝ \to A \cdot 0 = 0$
5	2 3 4	3eqtr3a	$⊢ A \in ℝ \to A -_{ℝ} A = 0$