Definition df-sub 10861

Description: Define subtraction. Theorem subval 10866 shows its value (and describes how this definition works), theorem subaddi 10962 relates it to addition, and theorems subcli 10951 and resubcli 10937 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 10859	. 2 class −
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cc 10524	. . 3 class ℂ
5	3	cv 1537	. . . . . 6 class 𝑦
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1537	. . . . . 6 class 𝑧
8		caddc 10529	. . . . . 6 class +
9	5, 7, 8	co 7135	. . . . 5 class (𝑦 + 𝑧)
10	2	cv 1537	. . . . 5 class 𝑥
11	9, 10	wceq 1538	. . . 4 wff (𝑦 + 𝑧) = 𝑥
12	11, 6, 4	crio 7092	. . 3 class (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)
13	2, 3, 4, 4, 12	cmpo 7137	. 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
14	1, 13	wceq 1538	1 wff − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))

This definition is referenced by:  subval  10866  subf  10877  sn-subf  39565