Metamath Proof Explorer


Definition df-subr

Description: Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012)

Ref Expression
Assertion df-subr - r = x V , y V v x v y v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminusr class - r
1 vx setvar x
2 cvv class V
3 vy setvar y
4 vv setvar v
5 cr class
6 1 cv setvar x
7 4 cv setvar v
8 7 6 cfv class x v
9 cmin class
10 3 cv setvar y
11 7 10 cfv class y v
12 8 11 9 co class x v y v
13 4 5 12 cmpt class v x v y v
14 1 3 2 2 13 cmpo class x V , y V v x v y v
15 0 14 wceq wff - r = x V , y V v x v y v