![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-sub | Unicode version |
Description: Define subtraction. Theorem subval 8145 shows its value (and describes how this definition works), Theorem subaddi 8240 relates it to addition, and Theorems subcli 8229 and resubcli 8216 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
Ref | Expression |
---|---|
df-sub |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmin 8124 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | cc 7806 |
. . 3
![]() ![]() | |
5 | 3 | cv 1352 |
. . . . . 6
![]() ![]() |
6 | vz |
. . . . . . 7
![]() ![]() | |
7 | 6 | cv 1352 |
. . . . . 6
![]() ![]() |
8 | caddc 7811 |
. . . . . 6
![]() ![]() | |
9 | 5, 7, 8 | co 5872 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 2 | cv 1352 |
. . . . 5
![]() ![]() |
11 | 9, 10 | wceq 1353 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11, 6, 4 | crio 5827 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 2, 3, 4, 4, 12 | cmpo 5874 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 1, 13 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: subval 8145 subf 8155 |
Copyright terms: Public domain | W3C validator |