Definition df-sub 7959

Description: Define subtraction. Theorem subval 7978 shows its value (and describes how this definition works), theorem subaddi 8073 relates it to addition, and theorems subcli 8062 and resubcli 8049 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 7957	. 2 class -
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cc 7642	. . 3 class CC
5	3	cv 1331	. . . . . 6 class y
6		vz	. . . . . . 7 setvar z
7	6	cv 1331	. . . . . 6 class z
8		caddc 7647	. . . . . 6 class +
9	5, 7, 8	co 5782	. . . . 5 class ( y + z )
10	2	cv 1331	. . . . 5 class x
11	9, 10	wceq 1332	. . . 4 wff ( y + z ) = x
12	11, 6, 4	crio 5737	. . 3 class ( iota_ z e. CC ( y + z ) = x )
13	2, 3, 4, 4, 12	cmpo 5784	. 2 class ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
14	1, 13	wceq 1332	1 wff - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )

This definition is referenced by:  subval  7978  subf  7988