How do you prove each $x$ for $a^x=y$ is unique? I'm not looking for limits or any calculus-related argument, I want to know how to prove uniqueness on a more fundamental level. I am at the point where I want to show $$a^x=a^y \implies x=y$$ but if I haven't yet proven the existence of a logarithm, how could it possibly be possible to show that $x=y$ ?
There is no way to get rid of that base $a$, but the fact that someone has already defined $\log_a(x)$ implies someone somehow did so some centuries ago. 
In other uniqueness arguments like of rational functions, you can manipulate both sides with rational operations, but you can't do that here because you haven't proven a logarithm yet! So how could anyone possibly show $x=y$ for $x>0$, $y>0$. 
Unless, can I use the properties of a logarithm after only making an argument for the existence of $x$ such that $a^{x}=y$ even if I haven't yet proven uniqueness and then use the existence to prove uniqueness for $a \neq 1$?
 A: Without knowing about logarithms, the question need not even begin to make sense, since it is unclear just what $a^x$ might mean, even for positive $a$, when $x$ is not restricted.
You say in the comments that you would define the function $f(x)=a^x$ simply as a function with the property that
$$\begin{align*}
f(1) &= a\\
f(x+y) &= f(x)f(y).
\end{align*}$$
However, these properties do not suffice to conclude that $f$ is one-to-one (which is required in order to conclude that $f(x)=f(y)$ implies $x=y$), or that there is a unique $x$ such that $f(x)=y$ for a given $y$ (or at most one such $x$ if you don't want to assume surjectivity).
In particular, if we assume the Axiom of Choice, then there are functions that satisfy both $f(1)=a$ and $f(x+y)=f(x)f(y)$, but that are not one to one.
"Explicitly" (modulo the Axiom of Choice), let $\beta$ be a basis for $\mathbb{R}$ as a vector space over $\mathbb{Q}$ such that $1\in\beta$. Then any function $g\colon \beta\to\mathbb{R}$ can be extended to an additive function $g\colon\mathbb{R}\to\mathbb{R}$; that is, a function defined on all of $\mathbb{R}$, whose values at $\beta$ are as specified, and such that for all $x,y\in\mathbb{R}$, we have $g(x+y)=g(x)+g(y)$.
Now, define $g\colon \beta\to\mathbb{R}$ by letting $g(1) = 1$ and $g(r)=0$ for all $r\in\beta$, $r\neq 1$. Then define $f\colon\mathbb{R}\to\mathbb{R}$ by $f(x) = a^{g(x)}$.
Then $f(1) = a^{g(1)} = a^1= a$; and $f(x+y) = a^{g(x+y)} = a^{g(x)+g(y)} = a^{g(x)}a^{g(y)} = f(x)f(y)$. So this function $f$ satisfies the two given equations.
However, $\beta$ is uncountable, so pick $r\neq 1$ that is in $\beta$. Then $f(r) = a^{g(r)} = a^0 = 1$, and $f(0) = 1$ (since $g(0)=0$ must hold for $g$ to be additive). However, $r\neq 0$, since $0$ cannot be an element of $\beta$.
Thus, the two conditions $f(1)=a$ and $f(x+y)=f(x)f(y)$ do not suffice to show that $f$ is one-to-one. 
Which means you need to specify a lot of other stuff; specifically, one need to know exactly what properties you are giving the function $f$.
(Yes, I know I'm using the exponential function to define this; but the point is that there are interpretations of the function $f$ that make all the assumptions true but the desired conclusion false, which means that one cannot prove the fact that $f$ is one-to-one using only the assumptions listed)

It is difficult to define either the exponential or the logarithm at the basic level of calculus-before-the-fundamental-theorem. 
One can define the exponential function by first defining the functions $a\longmapsto a^n$ with $n$ a positive integer, inductively. Then for $n$ a negative integer using reciprocals. Then for $n$ the reciprocal of a positive integer using inverse functions. Then for $n$ a rational using $a^{p/q} = (a^p)^{1/q}$. Then prove that if $\frac{p}{q}=\frac{r}{s}$ with $p,q,r,s$ integers, $r,s\gt 0$, then we get $a^{p/q}=a^{r/s}$. Then define $a^x$ for arbitrary $x$ by letting $(q_n)$  be a sequence of rationals such that $q_n\to x$ as $n\to\infty$, and showing that the sequence $a^{q_n}$ is Cauchy and converges to a number we call $a^x$. Then showing that if $(q_n)$ and $(r_n)$ are two sequences of rationals that both converge to $x$, then $\lim_{n\to\infty} a^{q_n} = \lim_{n\to\infty} a^{r_n}$. And once all of this has been done, then one can show that the function is stricitly monotone when $a\gt 0$, $a\neq 1$, to deduce what you want (and hence that it has an inverse and logarithms exist).
Obviously, this requires a lot of work.
Or one can use integrals and define the natural logarithm by
$$\ln(x)  = \int_1^x \frac{1}{t}\,dt$$
for $x\gt 0$. Using the Fundamental Theorem of Calculus one can show that this function is continuous and differentiable; using the properties of the integral that it is strictly increasing, and so has an inverse. Call the inverse the exponential function $\exp(x)$; and then define $a^x = \exp(x\ln(a))$. And then prove that this function is strictly monotone when $a\gt 0$, $a\neq 1$. 
This requires enough Calculus to prove the Fundamental Theorem of Calculus first. Again, a lot of work.

"Someone did it centuries ago"... The logarithm is a pretty recent "invention" as these things go, and it is closely connected with the development of calculus. Actual formal proofs of its properties (as well as actual formal proofs of the properties of the general exponential function) date from after the invention of calculus, and generally require some analysis or some calculus. I don't think you can really prove this via "elementary", non-analysis, non-calculus methods. 
A: $a^x$ is increasing for $a > 1$ and decreasing for $0 < a < 1$.
If $a^x = a^y$ then,
if you have the usual properties of power,
$a^{x-y} = 1$.
If $a^{x-y} = 1$ and $x \ne y$
then
$a^{n(x-y)} = 1$
for all integral $n$.
It all depends on what you know
about the $a^x$ function.
A: You touch on a very important problem regarding the mathematical concept of functions. Your question of whether $a^x=a^y$ implies $x=y$ is a special case of the more general question of whether $f(x)=f(y)$ implies $x=y$, for a certain function $f$. We have the following important definition:

A function $f$ taking real arguments is called injective if $f(a)=f(b)$ for real numbers $a$ and $b$ implies that $a=b$.

This definition extends to functions of complex numbers, as well as functions over arbitrary sets as well, but let's not worry about that for now. Indeed, if a function $f$ is injective, then we can define an inverse function $f^{-1}$ by $f^{-1}(f(a))=a$ for all real numbers $a$.
Our question of whether $a^x=a^y$ implies $x=y$ now comes down to the question of whether $f(x)=a^x$ is an injective function. For $a>0$ with $a\neq1$, the answer is yes. An easy way to convince yourself of this is by drawing the graph. For a sufficiently nice injective function $f$, drawing the graph $y=f(x)$ will reveal that every line parallel to the $x$-axis will intersect the graph at at most one point. This is because every such line is of the form $y=b$ for a constant $b$, and $b=f(x)$ implies $x=f^{-1}(b)$, which is a unique value. This is known as the horizontal line test. Now if we draw the graph considering the two cases where $0<a<1$ and where $a>1$, and then apply the horizontal line test, you should be able to see easily that $f$ is indeed injective.

Note: The so-called horizontal line test is not really rigorous at all. A more rigorous way of showing that $f$ is injective is by showing that it is strictly monotonic; that is, $x>y$ implies $a^x>a^y$. This is what Miguel Boto and marty cohen's answers do.
A: $$a^x = a^y ⇒ a^x * \frac{1}{a^y} = 1 ⇒ a^{x-y} = 1 ⇒ a^{x-y} = a^0 ⇒ x-y = 0 ⇒ x = y$$
This is true only if a ≠ o and a ≠ 1. 
If a = 1, then x ≠ y.
If a = 0, then $$a^{x-y} ≠ 1$$
A: Exponential functions are $1-1$.
Therefore, $a^{x} = a^{y}$ if and only if $x = y$.
A: Based on the real analysis tag, I'll assume we're dealing with $a \in \mathbb{R}_{>0}$ and $x \in \mathbb{R}$. In order to prove something about the function $x \mapsto a^x$, we must know what $a^x$ means. I'll try to do this without invoking calculus concepts or defining a logarithm by taking an approach suggested by Arturo Magidin. Let's build up our notion of exponentiation.
First, if $x$ is constrained to the positive integers (I'll denote it by $x=n$), we define $a^n$ by $a*a* ...*a$, with $n$ repetitions of multiplication. If $x$ is a negative integer, we define $a^{-n} = \frac{1}{a^n}$. Injectivity of the map $n \mapsto a^n$ is clear by strict monotonicity for $a \neq 1$ (the map is even more obviously not injective for $a = 1$).
If $x$ is constrained to the rational numbers (I'll denote it by $x = q = \frac{n}{m}$ with $m$ positive), we must establish that for each $a \in \mathbb{R}_{>0}$ we may find a unique $b \in \mathbb{R}_{>0}$ such that $b^m$ = $a$. Once this is done, we may define $a^q = b^n$. It's easy to see that this is independent of the representation of $q$ as a ratio of integers. A straightforward way to observe the unique existence of such a $b$ is to consider that the map $y \mapsto y^m$ is continuous and monotone on $\mathbb{R}_{\geq 0}$, that $0^m =0$, and that $\lim_{y \to \infty} y^m = \infty$, so the intermediate value theorem gives existence and monotonicity gives uniqueness. By expressing any $q_1 = \frac{n_1}{m}$, $q_2 = \frac{n_2}{m}$ with a common denominator, we easily deduce strict monotonicity (and hence injectivity) of $q \mapsto a^q$ from the integer result.
Now, if $x \in \mathbb{R}$ is unconstrained and $a>1$, we consider the set $W^x_a := \{a^w : w \in \mathbb{Q}, w \leq x \}$. Recalling that $q \mapsto a^q$ for $q \in \mathbb{Q}$ is strictly increasing, we see that $W_a^x$ has an upper bound given by $a^q$ for any $q > x$, so its supremum exists (it is certainly nonempty). Thus, we may define $a^x = \sup (W_a^x)$. Now, if $x < y \in \mathbb{R}$, we may find $q_1,q_2 \in \mathbb{Q}$ such that $x<q_1<q_2<y$, and hence for any rational $w \leq x$ we have $a^w <a^{q_1}$, showing $a^{q_1}$ is an upper bound for $W_a^x$, so $a^x \leq a^{q_1} < a^{q_2} \leq a^y$ (since $a^{q_2} \in W_a^y$). This shows that $x \mapsto a^x$, according to this definition, is strictly monotone and hence injective, as desired. 
In the case $0<a<1$, one must take the infimum instead of the supremum and reverse some inequalities, but the result is the same.
Comments: This definition, while having the advantage of being relatively elementary, is a bit unwieldy. Indeed, I expect it would be annoying to prove results such as surjectivity onto $\mathbb{R}_{>0}$, the continuity of either $x \mapsto a^x$ or $a \mapsto a^x$, or the identity $(a^{x})^y = a^{xy}$, whereas these are nearly immediate in the standard approach of defining $a^x = \exp(x\ln(a))$ (once one has done the work of defining $\exp$ and $\ln$). Further, this definition doesn't lend itself at all to generalizing our considerations to complex numbers (or $a<0$). However, we can at least get 
$$a^{x}a^{y} = \sup(W_a^x) * \sup(W_a^y) = \sup(W_a^x W_a^y) = \sup(W_a^{x+y}) = a^{x+y}$$
(see this result) without much trouble. It's not difficult at all to show that this agrees with the definition given in the standard approach using the latter's continuity.
A: I would like to give a simple explanation.Let us consider a^x=a^y.
Which means aaa*-----(x times) = aaa*------- (y times).
It means aa   (x times)/aa  (y times) =1.
This is possible only when both numerator and denominator has same number of terms.
Which yields x=y.
