MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sub Structured version   Visualization version   GIF version

Definition df-sub 11494
Description: Define subtraction. Theorem subval 11499 shows its value (and describes how this definition works), Theorem subaddi 11596 relates it to addition, and Theorems subcli 11585 and resubcli 11571 prove its closure laws. (Contributed by NM, 26-Nov-1994.)
Assertion
Ref Expression
df-sub − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-sub
StepHypRef Expression
1 cmin 11492 . 2 class
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cc 11153 . . 3 class
53cv 1539 . . . . . 6 class 𝑦
6 vz . . . . . . 7 setvar 𝑧
76cv 1539 . . . . . 6 class 𝑧
8 caddc 11158 . . . . . 6 class +
95, 7, 8co 7431 . . . . 5 class (𝑦 + 𝑧)
102cv 1539 . . . . 5 class 𝑥
119, 10wceq 1540 . . . 4 wff (𝑦 + 𝑧) = 𝑥
1211, 6, 4crio 7387 . . 3 class (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
132, 3, 4, 4, 12cmpo 7433 . 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
141, 13wceq 1540 1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
Colors of variables: wff setvar class
This definition is referenced by:  subval  11499  subf  11510  sn-subf  42458
  Copyright terms: Public domain W3C validator