Metamath Proof Explorer


Theorem subrfn

Description: Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012)

Ref Expression
Assertion subrfn A C B D A - r B Fn

Proof

Step Hyp Ref Expression
1 ovex A x B x V
2 eqid x A x B x = x A x B x
3 1 2 fnmpti x A x B x Fn
4 subrval A C B D A - r B = x A x B x
5 4 fneq1d A C B D A - r B Fn x A x B x Fn
6 3 5 mpbiri A C B D A - r B Fn