# 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}=\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼\left({v}\in ℝ⟼{x}\left({v}\right)-{y}\left({v}\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cminusr ${class}{-}_{r}$
1 vx ${setvar}{x}$
2 cvv ${class}\mathrm{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}\left({v}\right)$
9 cmin ${class}-$
10 3 cv ${setvar}{y}$
11 7 10 cfv ${class}{y}\left({v}\right)$
12 8 11 9 co ${class}\left({x}\left({v}\right)-{y}\left({v}\right)\right)$
13 4 5 12 cmpt ${class}\left({v}\in ℝ⟼{x}\left({v}\right)-{y}\left({v}\right)\right)$
14 1 3 2 2 13 cmpo ${class}\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼\left({v}\in ℝ⟼{x}\left({v}\right)-{y}\left({v}\right)\right)\right)$
15 0 14 wceq ${wff}{-}_{r}=\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼\left({v}\in ℝ⟼{x}\left({v}\right)-{y}\left({v}\right)\right)\right)$