Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-sub | Unicode version |
Description: Define subtraction. Theorem subval 8062 shows its value (and describes how this definition works), Theorem subaddi 8157 relates it to addition, and Theorems subcli 8146 and resubcli 8133 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
Ref | Expression |
---|---|
df-sub |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmin 8041 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | cc 7725 | . . 3 | |
5 | 3 | cv 1334 | . . . . . 6 |
6 | vz | . . . . . . 7 | |
7 | 6 | cv 1334 | . . . . . 6 |
8 | caddc 7730 | . . . . . 6 | |
9 | 5, 7, 8 | co 5821 | . . . . 5 |
10 | 2 | cv 1334 | . . . . 5 |
11 | 9, 10 | wceq 1335 | . . . 4 |
12 | 11, 6, 4 | crio 5776 | . . 3 |
13 | 2, 3, 4, 4, 12 | cmpo 5823 | . 2 |
14 | 1, 13 | wceq 1335 | 1 |
Colors of variables: wff set class |
This definition is referenced by: subval 8062 subf 8072 |
Copyright terms: Public domain | W3C validator |