![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-sub | GIF version |
Description: Define subtraction. Theorem subval 8151 shows its value (and describes how this definition works), Theorem subaddi 8246 relates it to addition, and Theorems subcli 8235 and resubcli 8222 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
Ref | Expression |
---|---|
df-sub | ⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmin 8130 | . 2 class − | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cc 7811 | . . 3 class ℂ | |
5 | 3 | cv 1352 | . . . . . 6 class 𝑦 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1352 | . . . . . 6 class 𝑧 |
8 | caddc 7816 | . . . . . 6 class + | |
9 | 5, 7, 8 | co 5877 | . . . . 5 class (𝑦 + 𝑧) |
10 | 2 | cv 1352 | . . . . 5 class 𝑥 |
11 | 9, 10 | wceq 1353 | . . . 4 wff (𝑦 + 𝑧) = 𝑥 |
12 | 11, 6, 4 | crio 5832 | . . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥) |
13 | 2, 3, 4, 4, 12 | cmpo 5879 | . 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
14 | 1, 13 | wceq 1353 | 1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
Colors of variables: wff set class |
This definition is referenced by: subval 8151 subf 8161 |
Copyright terms: Public domain | W3C validator |