Taking a theorem as a definition and proving the original definition as a theorem Gian-Carlo Rota's famous 1991 essay, "The pernicious influence of mathematics upon philosophy" contains the following passage:

Perform the following thought experiment. Suppose that you are given two formal presentations of the same mathematical theory.  The definitions of the first presentation are the theorems of the second, and vice versa.  This situation frequently occurs in mathematics.  Which of the two presentations makes the theory 'true'?  Neither, evidently: what we have is two presentations of the same theory.

Rota's claim that "this situation frequently occurs in mathematics" sounds reasonable to me, because I feel that I have frequently encountered authors who, after proving a certain theorem, say something like, "This theorem can be taken to be the definition of X," with the implicit suggestion that the original definition of X would then become a theorem.  However, when I tried to come up with explicit examples, I had a lot of trouble.  My question is, does this situation described by Rota really arise frequently in the literature?
There is a close connection between this question and another MO question about cryptomorphisms.  But I don't think the questions are exactly the same.  For instance, different axiomatizations of matroids comprise standard examples of cryptomorphisms.  It is true that one can take (say) the circuit axiomatization of a matroid and prove basis exchange as a theorem, or one can take basis exchange as an axiom and prove the circuit "axioms" as theorems.  But these equivalences are all pretty easy to prove; in Oxley's book Matroid Theory, they all appear in the introductory chapter.  As far as I know, none of the theorems in later chapters have the property that they could be taken as the starting point for matroid theory, with (say) basis exchange becoming a deep theorem.  What I'm wondering is whether there are cases in which a significant piece of theory really is developed in two different ways in the literature, with a major theorem of Presentation A being taken as a starting point for Presentation B, and the definitions of Presentation A being major theorems of Presentation B.
Let me also mention that I don't think that reverse mathematics is quite what Rota is referring to.  Brouwer's fixed-point theorem can be shown to imply the weak Kőnig's lemma over RCA0, but as far as I know, nobody seriously thinks that it makes sense to take Brouwer's fixed-point theorem as an axiom when developing the basics of analysis or topology.

EDIT: In another MO question, someone quoted Bott as referring to "the old French trick of turning a theorem into a definition". I'm not sure if Bott and Rota had exactly the same concept in mind, but it seems related.
 A: An example which is not quite what is being asked, and which is certainly much less sophisticated than the other answers, but which comes up in my calculus teaching around this week each year: continuity and the intermediate value theorem. High school students (at least in my country) are generally not given a limit definition of continuity; “the graph doesn't jump”, i.e. the conclusion of the IVT, is their definition of continuity. The history of this conception of continuity, in relation to the epsilon–delta/preimage-of-open-set definitions, is explored by Barany in a Notices article Stuck in the middle. Every year, one of my most interesting pedagogical challenges is to help students internalize the limit definition of continuity by seeing how it makes the IVT less obvious.
A: From a conversation I had with Gian-Carlo Rota when I was undergraduate, I know that one simple but important example that he specifically had in mind was the calculus of vector fields (whether specifically in three dimensions or more generally).  The gradient, divergence, and curl of differentiable fields on ${\mathbb R}^{3}$ can be defined as particular combinations of partial derivatives—in which case it is necessary to prove that they represent geometrical objects (meaning they transform correctly).  Alternatively, it is possible to specific purely geometrical definitions of all three objects, in which case it is necessary to prove that, when applied to sufficiently smooth functions, the can be calculated entirely in terms of partial derivatives.  Whichever way you like to approach the theory, it is possible to find textbooks that take your preferred starting point and do a good job of explaining vector calculus—even though the two approaches are, philosophically, quite different in terms of what they seem to assume about what, say, $\operatorname{grad} f$ "really means."  Moreover, there are also plenty of important theorems that can be proven from either starting point, without proving the equivalence first.
Somebody else, in the course of that conversation, mentioned the logarithm as an even more basic example.  There are actually many ways of initially defining the logarithm, and Calculus by James Stewart (or the first edition, at least) actually demonstrates explicitly that you can begin with the logarithm as the inverse of the exponential, or you can define $\ln x=\int_{1}^{x}(1/t)\,dt$ and eventually prove all the same things.
A: I recall multiple different definitions of holomorphic functions in several Complex Analysis textbooks, one by Ahlfors, one by Conway, and a couple more in Russian language textbooks.
One definition of a holomorphic function was based on Cauchy-Riemann equation, one starts from being locally analytic, one from angle preservating maps, and one from vanishing integral over closed curves.
And, of course, each textbook derived all other definitions as theorems.
A: Brendan McKay commented, "Any time we see a theorem that says 'the following are equivalent' followed by a list of statements, any one of the statements can be taken as a definition and the rest as theorems."
As a simple example, consider several equivalent definitions of Appell polynomial sequences (e.g., the Hermite and Bernoulli polynomials) $A_n(x)$ with the moment e.g.f. $A(t)=e^{a.t}$ with $a_0=1$ via an
1) e.g.f. (using the umbral maneuver $(A.(x))^n = A_n(x)$)
$$e^{A.(x) t} = A(t) \; e^{xt}$$
2) binomial convolution
$$A_n(x) = (a.+x)^n = \sum_{k=0}^n \; \binom{n}{k} \; a_k \; x^{n-k} $$
3) shift op
$$A_n(x) = A(\frac{d}{dx}) \; x^n = e^{a. \frac{d}{dx}} \; x^n$$
4) translation property
$$A_{n}(x+y) = (A.(x)+y)^n$$
5) recursion relation (via the formal cumulants $(c.)^k =c_k$ )
\begin{multline*}
e^{c.t} = \ln[A(t)]\quad\text{and} \\
A_{n+1}(x) = (x+c_1) \; A_n(x) + \sum_{k=1}^n \; \binom{n}{k} \; c_{k+1} \; A_{n-k}(x)
\end{multline*}
6) lowering op, given any Appell polynomial of order $n$, the lower order polynomials are defined by
$$\frac{d}{dx} \; A_n(x) = n \; A_{n-1}(x)$$
7) raising op
$$ R \; A_n(x) = A_{n+1}(x),$$
$$ R  = x + \frac{d}{dt} \ln[A(t)] \; |_{t= \frac{d}{dx}}$$
8) a diagonally multiplied Pascal matrix, the first few rows being
$$ [A] = \begin{pmatrix}
1 & 0 & 0 & 0 \\ 
a_1 & 1 & 0 & 0\\ 
a_2 & 2a_1 & 1 & 0\\ 
a_3 & 3a_2 & 3a_1 & 1
\end{pmatrix}$$
9) a 'probability density function' $pdf(u)$, if it exists, that generates the moments $(a.)^n = a_n$,
$$A_n(x) = \int (u +x)^n \; pdf(u) \; du $$
$$= \sum_{k=0}^n \binom{n}{k} \; x^{n-k} \; \int \; u^k \; pdf(u) \; du = (x +a.)^n$$
Having many equivalent definitions/reps could be taken as a definition of a 'rich' mathematical construct. The historical development of determinants/matrices from Cayley and Sylvester in invariant theory to their use in symmetric function theory, in definition of special functions, in the theory of characteristic classes, and in quantum mechanics bears this out. Recognition of their utility in diverse areas of mathematics and physics evolved gradually hand-in-hand with equivalent definitions/perspectives.
A: Many of the standard abstract mathematical structures were first defined and studied "externally" (in terms of some sort of concrete representation) and only later defined "internally" (as abstract spaces obeying some list of axioms), after a foundational theorem had been established demonstrating the equivalence of the two definitions.  For instance (oversimplifying the history a little bit to emphasise the point):

*

*Groups were first defined as permutation groups, or as groups that could be represented by permutations.  It was only with Cayley's theorem that one could equivalently define such groups in terms of the modern group axioms.

*In the early study of manifolds (e.g., by Poincaré), these spaces were often understood to be subspaces of some ambient Euclidean space, as opposed to the modern internal definition using atlases of coordinate charts, etc..  With the advent of embedding theorems such as the Whitney embedding theorem (for smooth manifolds) or Nash embedding theorem (for Riemannian manifolds), one could relate the two types of definitions.  In a similar spirit, Gauss's theorema egregium equates the external and internal definitions of what we now call Gauss curvature.

*Lie algebras were initially studied as algebras of linear transformations, often finite dimensional in nature.  The modern abstract definition came later, with theorems such as Ado's theorem and its relatives (Poincaré-Birkhoff-Witt theorem, Engel's theorem, Lie's theorem, etc.) providing fundamental equivalences between the two viewpoints.  I believe the history of von Neumann algebras follows a similar trajectory, though I am less familiar with this story.

*Boolean algebras are an interesting case in that (from my understanding of the history), Boole introduced the abstract concept of this algebra first, before the realisation that concrete Boolean algebras of sets obeyed Boole's axioms.  Nowadays of course, due to Stone's theorem, the two definitions can be viewed as equivalent.

*Probability spaces are still commonly defined today using a concrete representation (a sample space $\Omega$, equipped with a sigma-algebra of events and a probability measure).  But these spaces (up to almost sure equivalence) can be equated also with commutative tracial von Neumann algebras, thanks to the classification theory of the latter.  This equivalent definition is the most convenient starting point for introducing noncommutative probability spaces, which do not enjoy a classical representation in terms of sample spaces (though, thanks to the GNS construction, one can still interpret them in terms of algebras of bounded operators on a Hilbert space).

A: See the question Geometric interpretation of trace. There are several ways to define the trace:

*

*The sum of elements on the main diagonal.


*The sum of eigenvalues.


*The derivative of the determinant at the identity.


*The unique Lie algebra homomorphism onto $\mathbb{R}$, up to scale. (See also here.)


*"What you get when a linear map eats itself", as one answer put it. More precisely:

The idea of the trace operation is easily seen in string diagram notation: essentially one takes the endomorphism $a \stackrel{f}{\to} a$, "bends it around" using the duality and the symmetry and connects its output to its input.

This comment tells a story about it:

This reminds me of a story recounted by a friend of mine in graduate school. He spent a lot of time in the department, and one evening was approached by an undergraduate taking a fancy class that had introduced the trace of a linear transformation in the slick coordinate-free manner. This undergraduate had been tasked with computing the trace of a certain 2×2 matrix and had no idea how to proceed.

Nontrivial divides between coordinate-free/abstract and coordinate-based/concrete approaches—turning theorems into definitions and viceversa—also arise elsewhere, such as when defining tensors and tensor products.
A: If a module $M$ over a ring $R$ has a finite presentation (i.e. is the quotient of a module of finite type by a submodule which is also of finite type), then the functor $Hom_R(M,-)$ commutes with filtered colimits. The converse is true: if the functor $Hom_R(M,-)$ preserves filtered colimits, then $M$ has a finite presentation.
Remark: The possibilty of determining an object through finitely many generators and relations can very often characterized by the property the taking maps out of it is compatible with filtered colimits/unions (e.g. for groups, rings, and so on). Taking the property that $Hom(M,-)$ preserves filtered colimits as a definition is the notion of object of finite presentation in any category, which make sense even if there are no generators nor relations to discuss. Studying categories which are generated by objects of finite presentation is thus a natural thing to do. Replacing filtered diagrams by $\kappa$-filtered ones for various cardinals $\kappa$, this naturally leads to the theory of presentable categories, which is a major branch of category theory (being in the background of the theory of Grothendieck topoi, for instance), so robust that is has a counterpart in $\infty$-category theory. Developping this kind of ideas in a derived/homotopical context has also proved to be very useful (e.g. the notion of prefect complex of quasi-coherent sheaves).
A: This isn't an answer, so much as a string of hopefully-relevant observations:
Your question feels related to the distinction between analytic and synthetic mathematics. The former defines all objects and properties in terms of an existing theory, while the latter's core objects and properties are introduced as axioms. For example, analytic geometry is associated with Descartes - describing points, lines etc. in terms of co-ordinates and equations - and synthetic geometry with Euclid and Hilbert.
Personally, I associate the analytic approach with exploration: we find some examples of the things we're interested in, work out how to specify them (definitions in terms of an existing theory), study them as the concrete objects they are, and "pseudo-empirically" discover results which we then establish more reliably with proofs. Meanwhile, the synthetic approach takes some things that we already have a good feel for - in Euclid's case from everyday life, but these days more often from playing around analytically - and tries to extract their "essence" in the form of axioms so that we can prove results about them without worrying about concrete details of "implementation".
These associations 1  are conceptual only, and not hard-and-fast rules. Still, they suggest a way to think about your question:
In the "explorative" analytic approach, we might happen upon one specification first, discover that it implies another result, and then when investigating that result in its own right find that it leads back to the original specification. Meanwhile, in the synthetic approach, if two formalizations using the same language are truly equivalent then they will have exactly the same consequences, and in some sense it's the consequences that "matter": we could if we wished take both as primitive, along with the machinery needed to translate between them, and then observe that our choice of primitives contains redundancies (but the choice of which to discard, if any, is arbitrary). I think this is what Rota was getting at.
1 There are other lurking associations too, e.g. between analytic mathematics and (material) set theory or Platonism, and between synthetic mathematics and category theory or formalism. But of course any philosophical stance or background theory is compatible with both approaches.
A: One of the other answers briefly mentions tensors, but I think it’s a perfect answer to the question and deserves expansion. Tensors can be defined in several ways that are equivalent, but one’s choice of definition strongly influences how one thinks of tensors.
Tensor products of vector spaces can be defined by:

*

*Universal property,


*Span of $(v_1 \otimes \dotsb \otimes v_n)$s, with some multilinearity relations,


*Space of multidimensional arrays (i.e., with choices of ordered bases for the factor spaces), or


*Gadgets that eat vectors and/or covectors, and spit out some other vectors (or covectors or numbers).
Similar definitions are available for tensor fields (or tensor products of bundles), and in that case there is additionally the "definition" of a tensor field as


*An object that transforms in certain ways under changes of coordinates.

A: Several model-theoretic properties have multiple equivalent definitions. For a basic example, a theory $T$ is stable if

*

*there exists $\kappa\ge\|T\|$ such that for any model $M\models T$ and $A\subseteq M$ of size $|A|\le\kappa$, there are at most $\kappa$ complete types over $A$, or equivalently,


*there do not exist a formula $\phi(\bar x,\bar y)$, a model $M\models T$, and tuples $\{\bar a_n:n\in\omega\}$ in $M$ such that
$$M\models\phi(\bar a_i,\bar a_j)\iff i<j$$
for all $i,j\in\omega$.
You can start developing stability theory taking either property as a definition, and eventually deriving the other as a theorem.
A: The concept of a Sturmian word admits several equivalent definitions which one can work with, and which are not obviously equivalent.
A: Not a specific example, but the fact that this is common in mathematics is evident from the fact that mathematicians use the acronym TFAE, or "the following are equivalent", when stating that multiple propositions can each be derived from each other. I recall there were many theorems of the form below in my lectures as an undergraduate:

TFAE:

*

*(the definition)

*(some property)

*(some other property)
...


The first item in the list is usually a statement of the definition of a concept, and the remaining items in the list would be theorems which can be proved from the definition; but "TFAE" means the proofs can be done in any direction, so any individual item in the list would be usable as a definition.
In cases where there isn't a longer list of equivalent formulations, a theorem might be labelled as an "alternative definition".
A: There are two completely different "representation theorems" (one famous, one not so famous) for functions of bounded variation.  They yield the same theory and are ultimately connected (via the below centred equation), though this connection is not obvious at first glance.  Here is the short version:
On one hand, the most basic result for functions $f:[0,1]\rightarrow \mathbb{R}$ of bounded variation is the Jordan decomposition theorem (see here), namely that $f=g-h$ where $g, h$ are monotone functions, one of which can be taken to be $\lambda x.V_0^x(f)$, where the latter is the variation of $f$ on $[0,x]$ for $x\in (0,1]$.
On the other hand, Banach proves the following surprising result (for continuous functions, but it can be generalised to any function of bounded variation):
$$
V_{a}^{b}(f)=\int_{\mathbb{R}} N(f)(y) dy, \text{ where $N(f)(y)=\# \{x\in [a,b ]: f(x)=y\}$},
$$
where $N(f)$ is the Banach indicatrix.  To define $N(f)$ for discontinuous $f$ of bounded variation, one uses Sierpinski's decomposition theorem, implying that for $f$ of bounded variation, there is continuous $g$ and strictly increasing $h$ with $f=g\circ h$.  One can show that $N(g)=N(f)$ for such functions.
A: In ergodic theory, the conclusion of the Shannon-MacMillan-Breiman theorem about the pointwise growth rates of measures of cylinder sets, $h(\mu)=-\lim_{n\to\infty}1/n\log \mu([x_0\ldots x_{n-1}])$ almost everywhere, valid for ergodic shift-invariant measures is often taken as a definition of measure-theoretic entropy.
A: In set theory, measurable cardinals can be defined in two quite different ways. In the original 1930 definition, an uncountable cardinal $\kappa$ is measurable if its powerset $\mathcal{P}(\kappa)$ has a nonprincipal ultrafilter closed under meets of $<\kappa$-many elements.
In the 1960s, enough tools, techniques and concepts were developed to prove a theorem characterizing measurables in what seems to be an intrinsically 2nd-order way that quantifies over proper classes:
$\kappa$ is measurable iff there is a (nontrivial) elementary embedding $j\colon V\rightarrow M$ of the universe $V$ into a model $M$ such that $\kappa$ is the critical point of $j$ — the least ordinal $\alpha$ such that $j(\alpha) \neq \alpha$.
For expository purposes the original definition is usually preferred. But it's the latter characterization that has been generalized to define yet-larger cardinals, and it's not uncommon to see authors adopting it as their definition of 'measurable' in contexts where stronger notions are also considered.
A: I think the standard example is topological dimension:

*

*Dimension can be defined as either covering dimension, inductive dimension, or simplicial dimension. Then it is a theorem that dimension thus defined gives the same number as the other definitions.

The standard reference for this would probably have been Hurewicz and Wallman's Dimension Theory, published fifty years before Rota's article.
I'd guess that Rota was also thinking of homology theory:

*

*One can define homology as singular or simplicial homology. Then it is a theorem that homology thus defined has the same properties as with the other definitions, e.g. the Eilenberg-Steenrod axioms.

A: When I was teaching elementary geometry in high school in Holland 10 years ago, the concept of equivalent definitions was actually part of the curriculum. There the examples were more down to earth: you can either define a parallelogram as a quadrangle in which opposite sides have the same length and prove as a theorem that they are parallel, or as a quadrangle in which opposite sides are parallel and prove as a theorem that they are also of the same length.
Then you can also take the third standpoint of 'pick whichever definition you like best but justify this by proving as a theorem that both definitions are equivalent'.
Actually the third standpoint was kind of like the official school standpoint and we spent a lot of time trying to convey to the students that proving this latter theorem (of both definitions being equivalent) amounts to proving both the theorems mentioned above it.
I remember students found this 'equivalent definitions' stuff exceedingly confusing. This might however be partly be due to the fact that this short block of elementary geometry was the only time they had to work with definitions and proofs at all.
A: A Grothendieck topos can be defined either as the category of sheaves on a site, or as a category satisfying Giraud's axioms, or as an elementary topos that is bounded over $\rm Set$.  I believe any of these definitions can be taken as basic and a good deal of theory developed before proving the equivalence to the others.
For that matter, a sheaf on a topological space (or locale) $X$ can be defined either as a presheaf satisfying a gluing condition or as a local homeomorphism with codomain $X$.
A: Elementary geometry has switched between different approaches many times. From synthetic to analytic, from axiomatic to structural etc.
Euclid took additivity of magnitude, e.g. area, as its starting point. Hilbert builds the theory of area from first principles.
Euclid builds the number system from geometric data, whereas
nowadays it is customary in Cartesian geometry to start from a number system and build the geometry.
Classically, euclidean transformations are the ones that preserve lengths. Felix Klein showed how to build the euclidean invariants such as the length from the group itself.
Area, length and angles are the primary concepts in the Elements.
Nowadays the scalar product and orientation are taken as the basic definitions of an euclidean space in university courses.
It is quite interesting that what is an important theorem in a theory is close to being a definition in another one. I mentioned additivity of area. In the same fashion, the Pythagorean theorem is the last proposition of the first book of Euclid and its highest point. If one starts from a quadratic form, this is more or less a definition. Less known, Euclid actually proves that the plane has two dimension (prop. 7) from the additivity of angles. In modern approaches, a plan has two dimensions from its very definition and it is then deduced, sometimes painfully in cartesian coordinates, that the measure of angles is additive.
It is still a much heated debate which approach is the best with regards to teaching geometry to high school students.
A: A quite obvious, yet historically important example is represented by classical mechanics, in its Newtonian, Lagrangian and Hamiltonian presentations.
In particular, the field was widely reorganized (and a lot was discovered) when it was realized that stationarity of the action can be assumed as a principle.
Of course the example is not perfect, because the level of generality of these theories is not the same, but considering only sufficiently regular motions it becomes close to what you search for.
A: Rudin's Real and Complex Analysis begins by discussing the exponential function:

This is the most important function in mathematics. It is  defined, for  every  complex  number z,  by the formula
$$\exp(z)=\sum_{n=0}^{\infty}\frac{z^n}{n!}$$

A: A very basic example is the field $\mathbb{C}$ of complex numbers. -- It can be defined as the field one obtains when adjoining the square root of -1 to $\mathbb{R}$, in which case it needs to be proved as a theorem that every non-constant polynomial has a root / can be factored into linear factors. -- Or it can be defined as the algebraic closure of $\mathbb{R}$, in which case by definition every non-constant polynomial has a root / can be factored into linear factors, but it needs to be proved as a theorem that $\mathbb{C}$ can also be obtained from $\mathbb{R}$ by adjoining the square root of -1.
A: Example 1: In some textbooks, the trigonometric functions are defined via geometry. The advantage is that it is simpler to understand, but the disadvantage is that it is difficult to make completely rigorous without using integrals or at least a notion of area equivalent to the Jordan measure. In contrast, it is relatively easy to define them via their power series in a completely rigorous manner, and then prove their desired properties. Moreover, the first approach is restricted to $ℝ$, and we need to do something later to extend to $ℂ$, whereas in the second approach we can get the complex trigonometric functions directly. Nevertheless, both definitions (if done right) are equivalent.
Example 2: The Lebesgue measure has a number of equivalent definitions, as mentioned in Terence Tao's "An Introduction to Measure Theory". One definition is that a set $S⊆ℝ^n$ is measurable iff for every $ε>0$ there is some open set $G⊇S$ such that there is a countable sequence of boxes whose union contains $G∖S$ and whose total volume is at most $ε$. Another definition is the Caratheodory criterion; $S$ is measurable iff for every $A⊆ℝ^n$ we have $m^*(A) = m^*(A∩S)+m^*(A∖S)$, where $m^*$ is the outer measure. Although the Caratheodory criterion is unintuitive (as Tao also says), there are some textbooks that define the Lebesgue measure using that and then prove all the other equivalents.
A: [A] An example.
Construct the real numbers, for example some complicated thing using cuts.
Define addition, multiplication, ordering for the real numbers.
Prove the real numbers make up a complete ordered field.
Prove: any two complete ordered fields are isomorphic.
From then on, use only "complete ordered field", and never mention cuts again.
[B] Simpler
(1) An "ordered pair" is defined $\langle a,b \rangle = \{\{a\},\{a,b\}\}$.
(2) Prove $\langle a,b \rangle = \langle c,d\rangle$ if and only if
$a=c$ and $b=d$.
(3) From now on, use only the "defining property" (2).  After all, that is the motivation for (1) in the first place.
[C] Another
Prove the following are equivalent (in ZF):  (1) the axiom of choice (2) the well ordering princple (3) Zorn's lemma (4) Tukey's lemma (5) the Hausdorff maximality principle.
After that, when you say "ZFC" use any one of these.
(From Brendan McKay's comment.)
A: There seems to be plenty of such examples in the theory of Sobolev spaces and their refinements, such as Besov and Triebel-Lizorkin spaces, which have several definitions equivalent in non-obvious ways. One famous documentation of this is the H=W paper of Meyers and Serrin.
A: A couple elementary examples of this:
Greatest Common Divisor.
Consider the following two statements:
S1: The greatest common divisor $d=\gcd(a,b)$ satisfies: (i) $d \mid a$ and $d\mid b$ and (ii) if $c \mid a$ and $c \mid b$ then $c \mid d$.
S2: The greatest common divisor $d=\gcd(a,b)$ is the least positive element of the set $\{ax+by \mathrel\vert x,y \in \mathbb{Z}\}$.
I have seen textbooks define gcd with S1 and then prove S2 and I have seen textbooks define gcd with S2 and then prove S1.
Induction vs. Well-Ordering Principles
Likewise, axiomatic constructions of the natural numbers can choose to take the Principle of Induction:
$$((a \in S) \land ((\forall n \ge a)(n \in S \Rightarrow n+1 \in S))\Rightarrow \{a,a+1,a+2,a+3,\dotsc\} \subseteq S$$ or the Well-Ordering Principle: $$(\forall S \in \mathcal{P}(\mathbb{N}), S \neq \emptyset)(\exists a \in S)(\forall s \in S)(a \le s)$$
as an axiom and then prove the other as a theorem.
A: In probability theory, the notion of independence of random variables is usually introduced as follows:
we say that two random variables $X, Y$ are independent if for any two real numbers $(x,y)$ one has:
$\mathbf{P} \{ X \le x ,  Y \le y \} = \mathbf{P} \{ X \le x \} \cdot \mathbf{P} \{ Y \le y \}$ (i.e, the CDF of the pair $(X,Y)$ is just the product of the CDFs of $X$ and $Y$).
However, if we go back to the formal definition of random variables as measurable functions, then independence basically means that the sigma algebras $\sigma (X)$ and $\sigma (Y)$ generated by $X, Y$ (i.e., $\sigma (A)$ is the smallest sigma algebra inside which $A$ is measurable) are independent.
This definition allows us to speak about independence of more general class of random variables, than just $\mathbf{R}^n$-valued ones'.
Since, the Borel sets can be formed from the sets of the form $( -\infty , x)$ by using the operations of taking complements, countable union and countable intersections, so the above property in terms of CDFs is equivalent to the definition of independence.
A: Another example would be a Tychonoff (or Tiknonov, if you prefer) space. It can defined, equivalently, as a completely regular $T_0$-space, as homeomorphic to a subspace of some generalized cube (that is, the product space $[0, 1]^S$ for some set $S$, or as homeomorphic to a subspace of a compact Hausdorff space.
A: "There are good reasons why the theorems should all be easy and the definitions hard." --Michael Spivak, Preface to "Calculus on Manifolds",   Addison-Wesley: 1965.
This may be a little off theme for the original question as it involves proving a theorem in different frameworks, rather than it being used as an definition in one of them.
I like the example of Stokes' Theorem.  In 3 dimensions Stokes' can be laboriously proved in terms of vector calculus - coordinates and partial derivatives.  Or one can build up the definitions  of differential forms and chains, whence Stokes follows as a special case of the higher dimensional Fundamental Theorem of Calculus.
A: From "An Elementary Treatise on Cross-ratio Geometry: With Historical Notes" by J. J. Milne, 1911, (pg. 10), a definition of the cross-ratio of four lines:

If we consider the four concurrent straight lines OA, OB, OC, OD, we define the compound ratio $\frac{\sin(A,C)}{\sin(A,D)}: \frac{\sin(B,C)}{\sin(B,D)}$ ... as the cross-ratio of the pencil O(ABCD).

The CR is preserved by linear fractional/Möbius transformations transformations, supplying a chararcterization of projective space starting with a definition of the CR in terms of angles.
Conversely, from "On Klein’s So-called Non-Euclidean geometry" by Norbert A’Campo and Athanase Papadopoulos:

The cross ratio of four points is a projective invariant, and in some sense it is a complete projective invariant, since a transformation of projective space which preserves the cross ratio of quadruples of aligned points is a projective transformation. Therefore, it is natural to try to define distances and angles using the cross ratio. This is what Klein did.

The authors assert that this forms the basis of Klein's characterization of hyperbolic, spherical, and Euclidean geometries--the three geometries with constant curvature (Euclidean and non-Euclidean)--as encompassed by projective space:

A much less known fact is that Klein, besides giving a formula for the distance function in hyperbolic geometry, gave formulae for the distance in spherical and in Euclidean geometry using the cross ratio, taking instead of the ellipse (or ellipsoid)
other kinds of conics. In the case of Euclidean geometry, the conic is degenerate. In this way, the formulae that define the three geometries of constant curvature are of the same type, and the constructions of the three geometries are hereby done in a unified way in the realm of projective geometry.

