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?

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.
