Definition df-sub 8201

Description: Define subtraction. Theorem subval 8220 shows its value (and describes how this definition works), Theorem subaddi 8315 relates it to addition, and Theorems subcli 8304 and resubcli 8291 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 8199	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 7879	. . 3 class ℂ
5	3	cv 1363	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1363	. . . . . 6 class 𝑧
8		caddc 7884	. . . . . 6 class +
9	5, 7, 8	co 5923	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1363	. . . . 5 class 𝑥
11	9, 10	wceq 1364	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 5877	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 5925	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1364	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  8220  subf  8230  cndsex  14119