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

Step	Hyp	Ref	Expression
1		cmin 8029	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 7713	. . 3 class ℂ
5	3	cv 1334	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1334	. . . . . 6 class 𝑧
8		caddc 7718	. . . . . 6 class +
9	5, 7, 8	co 5818	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1334	. . . . 5 class 𝑥
11	9, 10	wceq 1335	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 5773	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 5820	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1335	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  8050  subf  8060