Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-sub | Unicode version |
Description: Define subtraction. Theorem subval 8111 shows its value (and describes how this definition works), Theorem subaddi 8206 relates it to addition, and Theorems subcli 8195 and resubcli 8182 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
Ref | Expression |
---|---|
df-sub |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmin 8090 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | cc 7772 | . . 3 | |
5 | 3 | cv 1347 | . . . . . 6 |
6 | vz | . . . . . . 7 | |
7 | 6 | cv 1347 | . . . . . 6 |
8 | caddc 7777 | . . . . . 6 | |
9 | 5, 7, 8 | co 5853 | . . . . 5 |
10 | 2 | cv 1347 | . . . . 5 |
11 | 9, 10 | wceq 1348 | . . . 4 |
12 | 11, 6, 4 | crio 5808 | . . 3 |
13 | 2, 3, 4, 4, 12 | cmpo 5855 | . 2 |
14 | 1, 13 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: subval 8111 subf 8121 |
Copyright terms: Public domain | W3C validator |