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

Metamath Proof Explorer

Theorem re0m0e0

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

		Ref	Expression
	Assertion	re0m0e0	$⊢ 0 -_{ℝ} 0 = 0$

Step	Hyp	Ref	Expression
1		0red	$⊢ ⊤ \to 0 \in ℝ$
2		sn-00id	$⊢ 0 + 0 = 0$
3	2	a1i	$⊢ ⊤ \to 0 + 0 = 0$
4	1 1 3	reladdrsub	$⊢ ⊤ \to 0 = 0 -_{ℝ} 0$
5	4	mptru	$⊢ 0 = 0 -_{ℝ} 0$
6	5	eqcomi	$⊢ 0 -_{ℝ} 0 = 0$