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&gt;0$, $y&gt;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$?
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) &amp;= a\\
f(x+y) &amp;= 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.
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.