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

Definition df-sub 8031
 Description: Define subtraction. Theorem subval 8050 shows its value (and describes how this definition works), Theorem subaddi 8145 relates it to addition, and Theorems subcli 8134 and resubcli 8121 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 8029 . 2 class
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cc 7713 . . 3 class
53cv 1334 . . . . . 6 class 𝑦
6 vz . . . . . . 7 setvar 𝑧
76cv 1334 . . . . . 6 class 𝑧
8 caddc 7718 . . . . . 6 class +
95, 7, 8co 5818 . . . . 5 class (𝑦 + 𝑧)
102cv 1334 . . . . 5 class 𝑥
119, 10wceq 1335 . . . 4 wff (𝑦 + 𝑧) = 𝑥
1211, 6, 4crio 5773 . . 3 class (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
132, 3, 4, 4, 12cmpo 5820 . 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
141, 13wceq 1335 1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
 Colors of variables: wff set class This definition is referenced by:  subval  8050  subf  8060
 Copyright terms: Public domain W3C validator