Definition df-sub 11442

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

This definition is referenced by:  subval  11447  subf  11458  sn-subf  43136