Metamath Proof Explorer


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 − = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) )