Dedekind's theorem In "Was sind und was sollen die Zahlen?" Dedekind gives a noncircular
proof of the statement that a set is finite if and only if it cannot be
put in bijective correspondence with a proper subset.  By "circular" I
mean in this context that you should not prove it by simply saying that a
proper subset of a finite set will have a smaller cardinality; this
theorem should be taken as the ground for the well-definedness of the
finite cardinals.
Regarding the "only if" direction, which establishes that finite ordinals
are cardinals, was Dedekind the first to publish a proof of this?  Did
Frege give a proof independently?  Galileo?  Leibniz?  Some medieval monk
perhaps?  It would seem strange if this basic aspect of the concept of
number was not reflected upon for so many centuries.
 A: Regarding the narrower interpretation of your question, the fact that the finite numbers are not equinumerous with
any proper subset is also expressed as the classical
pigeon hole
principle.
And for this, the linked Wikipedia article asserts that "the first
formalization of the idea is believed to have been made by
Johann Dirichlet in 1834 under the name Schubfachprinzip
(drawer principle or shelf principle)," and this of course
pre-dates Dedekind.
One can easily prove it by induction on $n$, for if $n$ is
a minimal counterexample, with $f:n\to n$ injective but not
surjective, then one can easily construct a smaller
counterexample by considering and rearranging the action on
one point.
A: EDIT NOTE: Thanks to Asaf Karagila for pointing out an error in the previous set-up; now the emphasis is put on finiteness vs Dedekind finiteness. 
The notion of a finite ordinal is quite modern, and was only articulated after Cantor's invention of set theory and his investigations of various kinds of linearly ordered sets, especially well-ordered ones. Also
Moreover, in our modern axiomatic view of set theory, Dedekind's characterization of finiteness only works in the presence of the axiom of choice. 

More specifically, let us define a set $X$ to be Dedekind finite provided there is no bijection between $X$ and a proper subset of $X$; and to be finite iff there is no $n \in \Bbb{N}$ such that $X$ has cardinality $n$. We also define $X$ is infinite iff $X$ is not finite. Then we have:

(1) The implication "If $X$ is finite, then $X$ is Dedekind finite" is provable in $ZF$ (Zermelo-Fraenkel set theory without the axiom of choice). This implication is one of the versions of the Pigeon-hole principle (see Joel Hamkins' answer).
(2) The implication "If $X$ is Dedekind finite, then $X$ is finite" is provable in $ZFC$ = $ZF$ + $AC$ [the axiom of choice].
(3) However, the implication "If $X$ is Dedekind finite, then $X$ is finite" is not provable in $ZF$. This was established first by Paul Cohen, in the early 1960's, as one of the first impressive exhibits of his "forcing" technology. Indeed, as shown by Cohen, in the absence of the axiom of choice, it is possible to have an infinite Dedekind finite subset of $\Bbb{R}$. It is not hard to see that $X$ is not Dedekind finite iff $\Bbb{N}$ can be injected into $X$; so in Cohen's model there is an infinite subset of  $\Bbb{R}$ into which $\Bbb{N}$ cannot be injected.
Finally, according to the source below [p.45, footnote 4], Dedekind's definition was also independently proposed by C.S. Pierce. 
Fraenkel, Abraham A.; Bar-Hillel, Yehoshua; Levy, Azriel
Foundations of set theory. North-Holland, 1973.
PS. Euclid's "the whole is greater than a part" - one of the five "common notions" in the Elements - might be been argued to be a precursor of Dedekind's theorem. Also, the idea of reducing the notion of cardinality to 1-1 correspondences is referred to as Hume's Principle in some modern philosophical texts, based on Frege's attribution of the principle to the 18th century philosopher David Hume.
A: Bolzano's work on paradoxes of the infinite may be relevant in this context.
