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$$

Proof

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