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

Metamath Proof Explorer

Theorem subval

Description: Value of subtraction, which is the (unique) element x such that B + x = A . (Contributed by NM, 4-Aug-2007) (Revised by Mario Carneiro, 2-Nov-2013)

Ref Expression
Assertion subval ⊢ 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-sub ⊢ − = 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