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

Definition df-sub 7602
 Description: Define subtraction. Theorem subval 7621 shows its value (and describes how this definition works), theorem subaddi 7716 relates it to addition, and theorems subcli 7705 and resubcli 7692 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 7600 . 2 class
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cc 7295 . . 3 class
53cv 1286 . . . . . 6 class 𝑦
6 vz . . . . . . 7 setvar 𝑧
76cv 1286 . . . . . 6 class 𝑧
8 caddc 7300 . . . . . 6 class +
95, 7, 8co 5615 . . . . 5 class (𝑦 + 𝑧)
102cv 1286 . . . . 5 class 𝑥
119, 10wceq 1287 . . . 4 wff (𝑦 + 𝑧) = 𝑥
1211, 6, 4crio 5570 . . 3 class (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
132, 3, 4, 4, 12cmpt2 5617 . 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
141, 13wceq 1287 1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
 Colors of variables: wff set class This definition is referenced by:  subval  7621  subf  7631
 Copyright terms: Public domain W3C validator