Isometry wrt intrinsic metric iff differential local isometry I want to prove the following statement:

Let $S_1, S_2$ be path-connected surfaces (i.e. 2-dimensional smooth submanifolds) in $\mathbb R^3$ equipped with the respective intrinsic metrics $d_1, d_2$ (i.e. the distance between $x,y$ is the length of the shortest path connecting them). Show that for a smooth map $f: S_1 \to S_2$ is equivalent:
  $1)$ $f$ is an isometry, that is $d_2(f(x),f(y)) = d_1(x,y)$ for each $x,y \in S_1$
  $2)$ For each $x\in S_1$ the differential $df_x: T_xS_1 \to T_{f(x)}S_2$ is a linear isometry with respect to the first fundamental form.  

Attempt:
"=>": Let $x\in S_1$. We need to show $\forall v \in T_xS_1: \lVert df_x(v)\rVert = \lVert v \rVert.$ I thought about this for a while, but I don't know how I can relate that to what's given. I know that for $c:(-\varepsilon, \varepsilon)\to S_1, c(0) = x, c'(0) = v$ we have $df_x(v) = (f \circ c)'(0)$. Any help appreciated!
 A: I think I found a proof:
$"\Rightarrow"$: Let $x\in S_1, v \in T_xS_1$ and let $c: (-\epsilon, \epsilon) \to S_1$ be a curve such that $c(0) = x, c'(0) = v$. Now we have for each $\delta >0$ s.t. $[-\delta, \delta] \subseteq (-\epsilon, \epsilon):$ $$l(c|_{[-\delta, \delta]}) = l(f\circ c|_{[\delta, \delta]}) \implies \int_{-\delta} ^\delta \lVert c'(t)\rVert dt = \int_{-\delta}^\delta \lVert (f \circ c)'(t)\rVert dt $$
since our assumption implies that the length of curves is preserved under isometries. Now we want to show $\lVert df_x(v) \rVert = \lVert (f\circ c)'(0) \rVert = \lVert c'(0)\rVert = \lVert v \rVert$.
Assume not, WLOG $\lVert (f\circ c)'(0) \rVert < \lVert c'(0)\rVert$. By continuity, there exists $\delta > 0$ s.t. $$\forall t\in (-\delta, \delta): \quad g(t) := \lVert c'(t) \rVert - \lVert (f \circ c)'(t)\rVert > 0.$$ 
Integrating both sides from $-\delta$ to $\delta$ for $\delta$ small enough this is a contradiction to $(1)$. Hence our assumption was wrong and $\lVert df_x(v) \rVert = \lVert v \rVert$.
$"\Leftarrow"$: Assume $f$ is not an isometry. Then there exists a smooth curve $c:(-\epsilon, \epsilon)\to S_1$ with $l(c) \neq l(f \circ c)$. But that means $\exists t_0$ s.t. $\lVert c'(t_0) \rVert \neq \lVert (f\circ c)'(t_0) \rVert$.
Now let $\gamma:(-\epsilon, \epsilon) \to S_1, t\mapsto \gamma(t) := c(t-t_0)$ and define $v:= \gamma'(0) = c'(t_0)$.
Now $$\lVert v \rVert = \lVert c'(t_0) \rVert \neq \lVert (f\circ c)'(t_0) \rVert = \lVert df_{c(t_0)}(v) \rVert ,$$so $df_{c(t_0)}$ is not an isometry.
