Definition df-sub 4133

Description: Define subtraction. Theorem subval 4134 shows it value (and describes how this definition works), theorem subadd 4143 relates it to addition, and theorems subcl 4139 and resubcl 4174 prove its closure laws.

Assertion

Ref	Expression
df-sub	|- - = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})}

Distinct variable group(s):   x,y,z,w

Detailed syntax breakdown of Definition df-sub

Step	Hyp	Ref	Expression
1		cmin 4089	. 2 class -
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cc 4026	. . . . . 6 class CC
5	3, 4	wcel 1092	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y e. CC
9	5, 8	wa 196	. . . 4 wff (x e. CC /\ y e. CC)
10		vz	. . . . . 6 set z
11	10	cv 1089	. . . . 5 class z
12		vw	. . . . . . . . . 10 set w
13	12	cv 1089	. . . . . . . . 9 class w
14		caddc 4031	. . . . . . . . 9 class +
15	7, 13, 14	co 3001	. . . . . . . 8 class (y + w)
16	15, 3	wceq 1091	. . . . . . 7 wff (y + w) = x
17	16, 12, 4	crab 1204	. . . . . 6 class {w e. CC | (y + w) = x}
18	17	cuni 1919	. . . . 5 class U.{w e. CC | (y + w) = x}
19	11, 18	wceq 1091	. . . 4 wff z = U.{w e. CC | (y + w) = x}
20	9, 19	wa 196	. . 3 wff ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})
21	20, 2, 6, 10	copab2 3002	. 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})}
22	1, 21	wceq 1091	1 wff - = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})}

This definition is referenced by:  subval 4134

metamath.org