Definition df-sub 5510

Description: Define subtraction. Theorem subval 5511 shows it value (and describes how this definition works), theorem subaddi 5525 relates it to addition, and theorems subcli 5520 and resubcli 5593 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:   x,y,z,w

Detailed syntax breakdown of Definition df-sub

Step	Hyp	Ref	Expression
1		cmin 5446	. 2 class -
2		vx	. . . . . . 7 set x
3	2	cv 991	. . . . . 6 class x
4		cc 5386	. . . . . 6 class CC
5	3, 4	wcel 994	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 991	. . . . . 6 class y
8	7, 4	wcel 994	. . . . 5 wff y e. CC
9	5, 8	wa 221	. . . 4 wff (x e. CC /\ y e. CC)
10		vz	. . . . . 6 set z
11	10	cv 991	. . . . 5 class z
12		vw	. . . . . . . . . 10 set w
13	12	cv 991	. . . . . . . . 9 class w
14		caddc 5391	. . . . . . . . 9 class +
15	7, 13, 14	co 4021	. . . . . . . 8 class (y + w)
16	15, 3	wceq 992	. . . . . . 7 wff (y + w) = x
17	16, 12, 4	crab 1694	. . . . . 6 class {w e. CC | (y + w) = x}
18	17	cuni 2569	. . . . 5 class U.{w e. CC | (y + w) = x}
19	11, 18	wceq 992	. . . 4 wff z = U.{w e. CC | (y + w) = x}
20	9, 19	wa 221	. . 3 wff ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})
21	20, 2, 6, 10	copab2 4022	. 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})}
22	1, 21	wceq 992	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 5511  subopr 5524

Copyright terms: Public domain