What is the precise statement of the theorem that allows us to "localize" our knowledge of derivatives? Most introductory calculus courses feature a proof that
Proposition 1. For the function $f : \mathbb{R} \rightarrow \mathbb{R}$ such that $x \in \mathbb{R} \Rightarrow f(x)=x^2$ it holds that $x \in \mathbb{R} \Rightarrow f'(x)=2x$.
In practice though, we freely use the following stronger result.
Proposition 2. For all partial functions $f : \mathbb{R} \rightarrow \mathbb{R}$, setting $X = \mathrm{dom}(f)$, we have that for all $x \in X$, if there exists a neighborhood of $x$ that is a subset of $X$, call it $A$, such that $a \in A \Rightarrow f(a)=a^2$, then we have $f'(x)=2x$.
What is the precise statement of the theorem that lets us get from the sentences that we actually prove, like Proposition 1, to the sentences we actually use, like Proposition 2?
 A: I don't think it is much of an ugly head. The definition of the derivative is inherently local. It's not really a theorem, more an observation.
If you want to be very precise, you could see the following fact:

For any $f\colon X\to Y$ and any $x\in A\subseteq X$ where $A$ is open, the derivative of $f$ at $x$ exists if and only if the derivative of restriction of $f$ to $A$ exists at $x$, and in this case, they are equal.

(I deliberately did not specify what $X$ and $Y$ are, it is true for multivariate functions with real or complex arguments, functions defined on differentiable manifolds, and likely with any conceivable, sensible notion of derivative for which the formulation even makes sense.)
A: I’ll give a first try in answering this:
How about: Let $f : D_f → ℝ$ and $g : D_g → ℝ$ be differentiable in an open set $D ⊂ D_f ∩ D_g$. If $f|_D = g|_D$, then $f'|_D = g'|_D$.
I feel this is not what you want. Did I misunderstand you?
A: I think it is the other way about. This note was getting too long for a comment.
As in the answer by tomasz, the usual definition of the derivative is inherently local - so one computes the derivative at a particular point, within an open neighbourhood in which the function is defined. The second formulation is more what is being done, and the first is a convenient summary of the outcome of the calculation on a particularly nice function.
Defining the derivative as in the first formulation assumes that the derivative exists, for example. And that is not the case, even for some of the "nice" functions we use ($f(x)=\frac 1 x, \tan x$). The elementary use of the first formulation generally ignores such issues, and we all know what we mean.
But the machinery for getting this to work consistently and coherently involves seeing the derivative as an operator on a function space taking the function represented by $x^2$ to $2x$. The various strategies for doing this are beyond elementary.
