Definition df-sub 7935

Description: Define subtraction. Theorem subval 7954 shows its value (and describes how this definition works), theorem subaddi 8049 relates it to addition, and theorems subcli 8038 and resubcli 8025 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 7933	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 7618	. . 3 class ℂ
5	3	cv 1330	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1330	. . . . . 6 class 𝑧
8		caddc 7623	. . . . . 6 class +
9	5, 7, 8	co 5774	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1330	. . . . 5 class 𝑥
11	9, 10	wceq 1331	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 5729	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 5776	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1331	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  7954  subf  7964