Definition df-sub 9830

Description: Define subtraction. Theorem subval 9834 shows its value (and describes how this definition works), theorem subaddi 9930 relates it to addition, and theorems subcli 9918 and resubcli 9904 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 9828	. 2
2		vx	. . 3
3		vy	. . 3
4		cc 9511	. . 3
5	3	cv 1394	. . . . . 6
6		vz	. . . . . . 7
7	6	cv 1394	. . . . . 6
8		caddc 9516	. . . . . 6
9	5, 7, 8	co 6296	. . . . 5
10	2	cv 1394	. . . . 5
11	9, 10	wceq 1395	. . . 4
12	11, 6, 4	crio 6256	. . 3
13	2, 3, 4, 4, 12	cmpt2 6298	. 2
14	1, 13	wceq 1395	1

This definition is referenced by:  subval  9834  subf  9845