Definition df-sub 11414

Description: Define subtraction. Theorem subval 11419 shows its value (and describes how this definition works), Theorem subaddi 11516 relates it to addition, and Theorems subcli 11505 and resubcli 11491 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 11412	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 11073	. . 3 class ℂ
5	3	cv 1539	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8		caddc 11078	. . . . . 6 class +
9	5, 7, 8	co 7390	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1539	. . . . 5 class 𝑥
11	9, 10	wceq 1540	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 7346	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 7392	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1540	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  11419  subf  11430  sn-subf  42424