Definition df-sub

Description: Define subtraction. Theorem subval shows its value (and describes how this definition works), Theorem subaddi relates it to addition, and Theorems subcli and resubcli prove its closure laws. (Contributed by NM, 26-Nov-1994)

	Ref	Expression
Assertion	df-sub	⊢ − = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmin	⊢ −
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		vy	⊢ 𝑦
4		vz	⊢ 𝑧
5	3	cv	⊢ 𝑦
6		caddc	⊢ +
7	4	cv	⊢ 𝑧
8	5 7 6	co	⊢ ( 𝑦 + 𝑧 )
9	1	cv	⊢ 𝑥
10	8 9	wceq	⊢ ( 𝑦 + 𝑧 ) = 𝑥
11	10 4 2	crio	⊢ ( ℩ 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 )
12	1 3 2 2 11	cmpo	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) )
13	0 12	wceq	⊢ − = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) )