Definition df-sub 8192

Description: Define subtraction. Theorem subval 8211 shows its value (and describes how this definition works), Theorem subaddi 8306 relates it to addition, and Theorems subcli 8295 and resubcli 8282 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 8190	. 2 class -
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cc 7870	. . 3 class CC
5	3	cv 1363	. . . . . 6 class y
6		vz	. . . . . . 7 setvar z
7	6	cv 1363	. . . . . 6 class z
8		caddc 7875	. . . . . 6 class +
9	5, 7, 8	co 5918	. . . . 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 5872	. . 3 class ( iota_ z e. CC ( y + z ) = x )
13	2, 3, 4, 4, 12	cmpo 5920	. 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  8211  subf  8221