![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-sub | Unicode version |
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.) |
Ref | Expression |
---|---|
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 |
Colors of variables: wff setvar class |
This definition is referenced by: subval 9834 subf 9845 |
Copyright terms: Public domain | W3C validator |