Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-sub | Unicode version |
Description: Define subtraction. Theorem subval 7954 shows its value (and describes how this definition works), theorem subaddi 8049 relates it to addition, and theorems subcli 8038 and resubcli 8025 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
Ref | Expression |
---|---|
df-sub |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmin 7933 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | cc 7618 | . . 3 | |
5 | 3 | cv 1330 | . . . . . 6 |
6 | vz | . . . . . . 7 | |
7 | 6 | cv 1330 | . . . . . 6 |
8 | caddc 7623 | . . . . . 6 | |
9 | 5, 7, 8 | co 5774 | . . . . 5 |
10 | 2 | cv 1330 | . . . . 5 |
11 | 9, 10 | wceq 1331 | . . . 4 |
12 | 11, 6, 4 | crio 5729 | . . 3 |
13 | 2, 3, 4, 4, 12 | cmpo 5776 | . 2 |
14 | 1, 13 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: subval 7954 subf 7964 |
Copyright terms: Public domain | W3C validator |