Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-sub | Structured version Visualization version GIF version |
Description: Define subtraction. Theorem subval 10272 shows its value (and describes how this definition works), theorem subaddi 10368 relates it to addition, and theorems subcli 10357 and resubcli 10343 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
Ref | Expression |
---|---|
df-sub | ⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmin 10266 | . 2 class − | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cc 9934 | . . 3 class ℂ | |
5 | 3 | cv 1482 | . . . . . 6 class 𝑦 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1482 | . . . . . 6 class 𝑧 |
8 | caddc 9939 | . . . . . 6 class + | |
9 | 5, 7, 8 | co 6650 | . . . . 5 class (𝑦 + 𝑧) |
10 | 2 | cv 1482 | . . . . 5 class 𝑥 |
11 | 9, 10 | wceq 1483 | . . . 4 wff (𝑦 + 𝑧) = 𝑥 |
12 | 11, 6, 4 | crio 6610 | . . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥) |
13 | 2, 3, 4, 4, 12 | cmpt2 6652 | . 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
14 | 1, 13 | wceq 1483 | 1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
Colors of variables: wff setvar class |
This definition is referenced by: subval 10272 subf 10283 |
Copyright terms: Public domain | W3C validator |