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

Metamath Proof Explorer

Definition df-resub

Description: Define subtraction between real numbers. This operator saves a few axioms over df-sub in certain situations. Theorem resubval shows its value, resubadd relates it to addition, and rersubcl proves its closure. It is the restriction of df-sub to the reals: subresre . (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion df-resub ⊢ - ℝ = x ∈ ℝ , y ∈ ℝ ⟼ ι z ∈ ℝ | y + z = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cresub class - ℝ
1 vx setvar x
2 cr class ℝ
3 vy setvar y
4 vz setvar z
5 3 cv setvar y
6 caddc class +
7 4 cv setvar z
8 5 7 6 co class y + z
9 1 cv setvar x
10 8 9 wceq wff y + z = x
11 10 4 2 crio class ι z ∈ ℝ | y + z = x
12 1 3 2 2 11 cmpo class x ∈ ℝ , y ∈ ℝ ⟼ ι z ∈ ℝ | y + z = x
13 0 12 wceq wff - ℝ = x ∈ ℝ , y ∈ ℝ ⟼ ι z ∈ ℝ | y + z = x