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	⊢ −ℝ : ( ℝ × ℝ ) ⟶ ℝ

Proof

Step	Hyp	Ref	Expression
1		resubval	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 −ℝ 𝑦 ) = ( ℩ 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 ) )
2		rersubcl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 −ℝ 𝑦 ) ∈ ℝ )
3	1 2	eqeltrrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℩ 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 ) ∈ ℝ )
4	3	rgen2	⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( ℩ 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 ) ∈ ℝ
5		df-resub	⊢ −ℝ = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( ℩ 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 ) )
6	5	fmpo	⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( ℩ 𝑧 ∈ ℝ ( 𝑦 + 𝑧 ) = 𝑥 ) ∈ ℝ ↔ −ℝ : ( ℝ × ℝ ) ⟶ ℝ )
7	4 6	mpbi	⊢ −ℝ : ( ℝ × ℝ ) ⟶ ℝ