Definition df-sub 8280

Description: Define subtraction. Theorem subval 8299 shows its value (and describes how this definition works), Theorem subaddi 8394 relates it to addition, and Theorems subcli 8383 and resubcli 8370 prove its closure laws. (Contributed by NM, 26-Nov-1994.)

Assertion

Ref	Expression
df-sub	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-sub

Step	Hyp	Ref	Expression
1		cmin 8278	. 2 class -
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cc 7958	. . 3 class CC
5	3	cv 1372	. . . . . 6 class y
6		vz	. . . . . . 7 setvar z
7	6	cv 1372	. . . . . 6 class z
8		caddc 7963	. . . . . 6 class +
9	5, 7, 8	co 5967	. . . . 5 class ( y + z )
10	2	cv 1372	. . . . 5 class x
11	9, 10	wceq 1373	. . . 4 wff ( y + z ) = x
12	11, 6, 4	crio 5921	. . 3 class ( iota_ z e. CC ( y + z ) = x )
13	2, 3, 4, 4, 12	cmpo 5969	. 2 class ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
14	1, 13	wceq 1373	1 wff - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )

This definition is referenced by:  subval  8299  subf  8309  cndsex  14430