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 10870
Description: Define subtraction. Theorem subval 10875 shows its value (and describes how this definition works), theorem subaddi 10971 relates it to addition, and theorems subcli 10960 and resubcli 10946 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 10868 . 2 class
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cc 10533 . . 3 class
53cv 1537 . . . . . 6 class 𝑦
6 vz . . . . . . 7 setvar 𝑧
76cv 1537 . . . . . 6 class 𝑧
8 caddc 10538 . . . . . 6 class +
95, 7, 8co 7149 . . . . 5 class (𝑦 + 𝑧)
102cv 1537 . . . . 5 class 𝑥
119, 10wceq 1538 . . . 4 wff (𝑦 + 𝑧) = 𝑥
1211, 6, 4crio 7106 . . 3 class (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
132, 3, 4, 4, 12cmpo 7151 . 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
141, 13wceq 1538 1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
Colors of variables: wff setvar class
This definition is referenced by:  subval  10875  subf  10886  sn-subf  39498
  Copyright terms: Public domain W3C validator