rersubcl

Description: Closure for real subtraction. Based on subcl . (Contributed by Steven Nguyen, 7-Jan-2023)

		Ref	Expression
	Assertion	rersubcl	$⊢ (A \in ℝ \land B \in ℝ) \to A -_{ℝ} B \in ℝ$

Step	Hyp	Ref	Expression
1		resubval	$⊢ (A \in ℝ \land B \in ℝ) \to A -_{ℝ} B = (ι x \in ℝ \| B + x = A)$
2		resubeu	$⊢ (B \in ℝ \land A \in ℝ) \to \exists! x \in ℝ B + x = A$
3	2	ancoms	$⊢ (A \in ℝ \land B \in ℝ) \to \exists! x \in ℝ B + x = A$
4		riotacl	$⊢ \exists! x \in ℝ B + x = A \to (ι x \in ℝ \| B + x = A) \in ℝ$
5	3 4	syl	$⊢ (A \in ℝ \land B \in ℝ) \to (ι x \in ℝ \| B + x = A) \in ℝ$
6	1 5	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ) \to A -_{ℝ} B \in ℝ$

Metamath Proof Explorer