![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-sub | Unicode version |
Description: Define subtraction. Theorem subval 7000 shows its value (and describes how this definition works), theorem subaddi 7094 relates it to addition, and theorems subcli 7083 and resubcli 7070 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
Ref | Expression |
---|---|
df-sub |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmin 6979 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | cc 6709 |
. . 3
![]() ![]() | |
5 | 3 | cv 1241 |
. . . . . 6
![]() ![]() |
6 | vz |
. . . . . . 7
![]() ![]() | |
7 | 6 | cv 1241 |
. . . . . 6
![]() ![]() |
8 | caddc 6714 |
. . . . . 6
![]() ![]() | |
9 | 5, 7, 8 | co 5455 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 2 | cv 1241 |
. . . . 5
![]() ![]() |
11 | 9, 10 | wceq 1242 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11, 6, 4 | crio 5410 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 2, 3, 4, 4, 12 | cmpt2 5457 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 1, 13 | wceq 1242 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: subval 7000 subf 7010 |
Copyright terms: Public domain | W3C validator |