This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resubval

Description: Value of real subtraction, which is the (unique) real x such that B + x = A . (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion resubval ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ B = ι x ∈ ℝ | B + x = A

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ y = A → z + x = y ↔ z + x = A
2 1 riotabidv ⊢ y = A → ι x ∈ ℝ | z + x = y = ι x ∈ ℝ | z + x = A
3 oveq1 ⊢ z = B → z + x = B + x
4 3 eqeq1d ⊢ z = B → z + x = A ↔ B + x = A
5 4 riotabidv ⊢ z = B → ι x ∈ ℝ | z + x = A = ι x ∈ ℝ | B + x = A
6 df-resub ⊢ - ℝ = y ∈ ℝ , z ∈ ℝ ⟼ ι x ∈ ℝ | z + x = y
7 riotaex ⊢ ι x ∈ ℝ | B + x = A ∈ V
8 2 5 6 7 ovmpo ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ B = ι x ∈ ℝ | B + x = A