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 10866 shows its value (and describes how this definition works), theorem subaddi 10962 relates it to addition, and theorems subcli 10951 and resubcli 10937 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
Ref | Expression |
---|---|
df-sub | ⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmin 10859 | . 2 class − | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | cc 10524 | . . 3 class ℂ | |
5 | 3 | cv 1527 | . . . . . 6 class 𝑦 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1527 | . . . . . 6 class 𝑧 |
8 | caddc 10529 | . . . . . 6 class + | |
9 | 5, 7, 8 | co 7145 | . . . . 5 class (𝑦 + 𝑧) |
10 | 2 | cv 1527 | . . . . 5 class 𝑥 |
11 | 9, 10 | wceq 1528 | . . . 4 wff (𝑦 + 𝑧) = 𝑥 |
12 | 11, 6, 4 | crio 7102 | . . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥) |
13 | 2, 3, 4, 4, 12 | cmpo 7147 | . 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
14 | 1, 13 | wceq 1528 | 1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
Colors of variables: wff setvar class |
This definition is referenced by: subval 10866 subf 10877 |
Copyright terms: Public domain | W3C validator |