Definition df-sub 11308

Description: Define subtraction. Theorem subval 11313 shows its value (and describes how this definition works), Theorem subaddi 11409 relates it to addition, and Theorems subcli 11398 and resubcli 11384 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 11306	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 10970	. . 3 class ℂ
5	3	cv 1539	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		caddc 10975	. . . . . 6 class +
9	5, 7, 8	co 7337	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1539	. . . . 5 class 𝑥
11	9, 10	wceq 1540	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 7292	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 7339	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1540	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  11313  subf  11324  sn-subf  40670