Definition df-sub 8351

Description: Define subtraction. Theorem subval 8370 shows its value (and describes how this definition works), Theorem subaddi 8465 relates it to addition, and Theorems subcli 8454 and resubcli 8441 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

Step	Hyp	Ref	Expression
1		cmin 8349	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 8029	. . 3 class ℂ
5	3	cv 1396	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1396	. . . . . 6 class 𝑧
8		caddc 8034	. . . . . 6 class +
9	5, 7, 8	co 6017	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1396	. . . . 5 class 𝑥
11	9, 10	wceq 1397	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 5969	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 6019	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1397	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  8370  subf  8380  cndsex  14566