Definition df-sub 9589

Description: Define subtraction. Theorem subval 9593 shows its value (and describes how this definition works), theorem subaddi 9687 relates it to addition, and theorems subcli 9676 and resubcli 9663 prove its closure laws. (Contributed by NM, 26-Nov-1994.)

Assertion

Ref	Expression
df-sub

Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-sub

Step	Hyp	Ref	Expression
1		cmin 9587	. 2
2		vx	. . 3
3		vy	. . 3
4		cc 9272	. . 3
5	3	cv 1368	. . . . . 6
6		vz	. . . . . . 7
7	6	cv 1368	. . . . . 6
8		caddc 9277	. . . . . 6
9	5, 7, 8	co 6086	. . . . 5
10	2	cv 1368	. . . . 5
11	9, 10	wceq 1369	. . . 4
12	11, 6, 4	crio 6046	. . 3
13	2, 3, 4, 4, 12	cmpt2 6088	. 2
14	1, 13	wceq 1369	1

This definition is referenced by:  subval  9593  subf  9604