Definition df-sub 5328

Description: Define subtraction. Theorem subvalt 5329 shows it value (and describes how this definition works), theorem subadd 5343 relates it to addition, and theorems subcl 5338 and resubcl 5411 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 5264	. 2 class -
2		vx	. . . . . . 7 set x
3	2	cv 952	. . . . . 6 class x
4		cc 5204	. . . . . 6 class CC
5	3, 4	wcel 955	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 952	. . . . . 6 class y
8	7, 4	wcel 955	. . . . 5 wff y e. CC
9	5, 8	wa 223	. . . 4 wff (x e. CC /\ y e. CC)
10		vz	. . . . . 6 set z
11	10	cv 952	. . . . 5 class z
12		vw	. . . . . . . . . 10 set w
13	12	cv 952	. . . . . . . . 9 class w
14		caddc 5209	. . . . . . . . 9 class +
15	7, 13, 14	co 3948	. . . . . . . 8 class (y + w)
16	15, 3	wceq 953	. . . . . . 7 wff (y + w) = x
17	16, 12, 4	crab 1640	. . . . . 6 class {w e. CC | (y + w) = x}
18	17	cuni 2493	. . . . 5 class U.{w e. CC | (y + w) = x}
19	11, 18	wceq 953	. . . 4 wff z = U.{w e. CC | (y + w) = x}
20	9, 19	wa 223	. . 3 wff ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})
21	20, 2, 6, 10	copab2 3949	. 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})}
22	1, 21	wceq 953	1 wff - = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})}

This definition is referenced by:  subvalt 5329  subopr 5342

Copyright terms: Public domain