Definition df-sub 8506

Description: Define subtraction. Theorem subval 8525 shows its value (and describes how this definition works), Theorem subaddi 8620 relates it to addition, and Theorems subcli 8609 and resubcli 8596 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 8504	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 8183	. . 3 class ℂ
5	3	cv 1401	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1401	. . . . . 6 class 𝑧
8		caddc 8188	. . . . . 6 class +
9	5, 7, 8	co 6088	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1401	. . . . 5 class 𝑥
11	9, 10	wceq 1402	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 6040	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 6090	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1402	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is used by:  subval  8525  subf  8535  cndsex  14999