Definition df-sub 11449

Description: Define subtraction. Theorem subval 11454 shows its value (and describes how this definition works), Theorem subaddi 11551 relates it to addition, and Theorems subcli 11540 and resubcli 11526 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 11447	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 11104	. . 3 class ℂ
5	3	cv 1568	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1568	. . . . . 6 class 𝑧
8		caddc 11109	. . . . . 6 class +
9	5, 7, 8	co 7412	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1568	. . . . 5 class 𝑥
11	9, 10	wceq 1569	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 7368	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 7414	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1569	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is used by:  subval  11454  subf  11465  sn-subf  43218