Definition df-sub 11375

Description: Define subtraction. Theorem subval 11380 shows its value (and describes how this definition works), Theorem subaddi 11477 relates it to addition, and Theorems subcli 11466 and resubcli 11452 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 11373	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 11032	. . 3 class ℂ
5	3	cv 1547	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1547	. . . . . 6 class 𝑧
8		caddc 11037	. . . . . 6 class +
9	5, 7, 8	co 7359	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1547	. . . . 5 class 𝑥
11	9, 10	wceq 1548	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 7315	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 7361	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1548	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  11380  subf  11391  sn-subf  42919