Theorem 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⟶ℝ$$

Proof

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