Definition df-sub 7246

Description: Define subtraction. Theorem subval 7265 shows its value (and describes how this definition works), theorem subaddi 7360 relates it to addition, and theorems subcli 7349 and resubcli 7336 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 7244	. 2 class -
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cc 6944	. . 3 class CC
5	3	cv 1258	. . . . . 6 class y
6		vz	. . . . . . 7 setvar z
7	6	cv 1258	. . . . . 6 class z
8		caddc 6949	. . . . . 6 class +
9	5, 7, 8	co 5539	. . . . 5 class ( y + z )
10	2	cv 1258	. . . . 5 class x
11	9, 10	wceq 1259	. . . 4 wff ( y + z ) = x
12	11, 6, 4	crio 5494	. . 3 class ( iota_ z e. CC ( y + z ) = x )
13	2, 3, 4, 4, 12	cmpt2 5541	. 2 class ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
14	1, 13	wceq 1259	1 wff - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )

This definition is referenced by:  subval  7265  subf  7275