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