resubf

Description: Real subtraction is an operation on the real numbers. Based on subf . (Contributed by Steven Nguyen, 7-Jan-2023)

		Ref	Expression
	Assertion	resubf	$⊢ -_{ℝ} : ℝ^{2} ⟶ ℝ$

Step	Hyp	Ref	Expression
1		resubval	$⊢ (x \in ℝ \land y \in ℝ) \to x -_{ℝ} y = (ι z \in ℝ \| y + z = x)$
2		rersubcl	$⊢ (x \in ℝ \land y \in ℝ) \to x -_{ℝ} y \in ℝ$
3	1 2	eqeltrrd	$⊢ (x \in ℝ \land y \in ℝ) \to (ι z \in ℝ \| y + z = x) \in ℝ$
4	3	rgen2	$⊢ \forall x \in ℝ \forall y \in ℝ (ι z \in ℝ \| y + z = x) \in ℝ$
5		df-resub	$⊢ -_{ℝ} = (x \in ℝ, y \in ℝ ⟼ (ι z \in ℝ \| y + z = x))$
6	5	fmpo	$⊢ \forall x \in ℝ \forall y \in ℝ (ι z \in ℝ \| y + z = x) \in ℝ \leftrightarrow -_{ℝ} : ℝ^{2} ⟶ ℝ$
7	4 6	mpbi	$⊢ -_{ℝ} : ℝ^{2} ⟶ ℝ$

Metamath Proof Explorer