Definition df-sub 8194

Description: Define subtraction. Theorem subval 8213 shows its value (and describes how this definition works), Theorem subaddi 8308 relates it to addition, and Theorems subcli 8297 and resubcli 8284 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 8192	. 2 class -
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cc 7872	. . 3 class CC
5	3	cv 1363	. . . . . 6 class y
6		vz	. . . . . . 7 setvar z
7	6	cv 1363	. . . . . 6 class z
8		caddc 7877	. . . . . 6 class +
9	5, 7, 8	co 5919	. . . . 5 class ( y + z )
10	2	cv 1363	. . . . 5 class x
11	9, 10	wceq 1364	. . . 4 wff ( y + z ) = x
12	11, 6, 4	crio 5873	. . 3 class ( iota_ z e. CC ( y + z ) = x )
13	2, 3, 4, 4, 12	cmpo 5921	. 2 class ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
14	1, 13	wceq 1364	1 wff - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )

This definition is referenced by:  subval  8213  subf  8223  cndsex  14052