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
|- -R = ( x e. RR , y e. RR |-> ( iota_ z e. RR ( y + z ) = x ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cresub
 |-  -R
1 vx
 |-  x
2 cr
 |-  RR
3 vy
 |-  y
4 vz
 |-  z
5 3 cv
 |-  y
6 caddc
 |-  +
7 4 cv
 |-  z
8 5 7 6 co
 |-  ( y + z )
9 1 cv
 |-  x
10 8 9 wceq
 |-  ( y + z ) = x
11 10 4 2 crio
 |-  ( iota_ z e. RR ( y + z ) = x )
12 1 3 2 2 11 cmpo
 |-  ( x e. RR , y e. RR |-> ( iota_ z e. RR ( y + z ) = x ) )
13 0 12 wceq
 |-  -R = ( x e. RR , y e. RR |-> ( iota_ z e. RR ( y + z ) = x ) )