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-2022)

	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 ) )