ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-sub GIF version

Definition df-sub 7899
Description: Define subtraction. Theorem subval 7918 shows its value (and describes how this definition works), theorem subaddi 8013 relates it to addition, and theorems subcli 8002 and resubcli 7989 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 7897 . 2 class
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cc 7582 . . 3 class
53cv 1313 . . . . . 6 class 𝑦
6 vz . . . . . . 7 setvar 𝑧
76cv 1313 . . . . . 6 class 𝑧
8 caddc 7587 . . . . . 6 class +
95, 7, 8co 5740 . . . . 5 class (𝑦 + 𝑧)
102cv 1313 . . . . 5 class 𝑥
119, 10wceq 1314 . . . 4 wff (𝑦 + 𝑧) = 𝑥
1211, 6, 4crio 5695 . . 3 class (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
132, 3, 4, 4, 12cmpo 5742 . 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
141, 13wceq 1314 1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
Colors of variables: wff set class
This definition is referenced by:  subval  7918  subf  7928
  Copyright terms: Public domain W3C validator