Definition df-sub 11207

Description: Define subtraction. Theorem subval 11212 shows its value (and describes how this definition works), Theorem subaddi 11308 relates it to addition, and Theorems subcli 11297 and resubcli 11283 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 11205	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 10869	. . 3 class ℂ
5	3	cv 1538	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1538	. . . . . 6 class 𝑧
8		caddc 10874	. . . . . 6 class +
9	5, 7, 8	co 7275	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1538	. . . . 5 class 𝑥
11	9, 10	wceq 1539	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 7231	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 7277	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1539	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  11212  subf  11223  sn-subf  40410