Definition df-sub 7281

Description: Define subtraction. Theorem subval 7300 shows its value (and describes how this definition works), theorem subaddi 7395 relates it to addition, and theorems subcli 7384 and resubcli 7371 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 7279	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 6979	. . 3 class ℂ
5	3	cv 1283	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1283	. . . . . 6 class 𝑧
8		caddc 6984	. . . . . 6 class +
9	5, 7, 8	co 5532	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1283	. . . . 5 class 𝑥
11	9, 10	wceq 1284	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 5487	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpt2 5534	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1284	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  7300  subf  7310