Definition df-sub 5336

Description: Define subtraction. Theorem subvalt 5337 shows it value (and describes how this definition works), theorem subadd 5351 relates it to addition, and theorems subcl 5346 and resubcl 5419 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 5272	. 2 class -
2		vx	. . . . . . 7 set x
3	2	cv 953	. . . . . 6 class x
4		cc 5212	. . . . . 6 class CC
5	3, 4	wcel 956	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 953	. . . . . 6 class y
8	7, 4	wcel 956	. . . . 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 953	. . . . 5 class z
12		vw	. . . . . . . . . 10 set w
13	12	cv 953	. . . . . . . . 9 class w
14		caddc 5217	. . . . . . . . 9 class +
15	7, 13, 14	co 3954	. . . . . . . 8 class (y + w)
16	15, 3	wceq 954	. . . . . . 7 wff (y + w) = x
17	16, 12, 4	crab 1645	. . . . . 6 class {w e. CC | (y + w) = x}
18	17	cuni 2498	. . . . 5 class U.{w e. CC | (y + w) = x}
19	11, 18	wceq 954	. . . 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 3955	. 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})}
22	1, 21	wceq 954	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 5337  subopr 5350

Copyright terms: Public domain