Elliptic curves in Edwards form (or Edwards curve) and addition formulas In recent studies on elliptic curve cryptography, Edwards curves are remarkable examples on this field. Studies show that this kind of elliptic curves provide faster computation compared to Weierstrass form. 

The following equation is called an Edward Curve
$$x^2 + y^2 = 1 + d\cdot x^2\cdot y^2$$
or $$x^2 + y^2 = c^2 \cdot (1+d\cdot x^2y^2)$$

If $(x_1, y_1)$ and $(x_2, y_2)$ are points on an Edwards curve, then new point calculated by addition formula would be still on the curve as illustrated below.

$$(x_1, y_1) + (x_2, y_2) = (x_3, y_3)$$
where:

$$\begin{align}
x_3 &amp;= \frac{(x_1\cdot y_2+x_2\cdot y_1)}{(1+d\cdot x_1\cdot x_2\cdot y_1\cdot y_2)}\\
y_3 &amp;=  \frac{(y_1\cdot y_2-x_1\cdot x_2)}{(1-d\cdot x_1\cdot x_2\cdot y_1\cdot y_2)}\\
\end{align}$$

Proofs of addition formulas for conventional Weierstrass form exist. However, I cannot find any proof for Edwards curve addition formulas. Where do they come from?
I think this is a good question, but not one with an easy answer. Let me give it a go anyway.

First of all, let's focus on the classic Weierstrass case. The points on an elliptic curve $E$ in this shape form a group. We can do this by the standard way (in most cases): draw a line between two points $P$ and $Q$, intersect at a unique third point, and invert across the $x$-axis. The resulting point $R$ is defined to be $P+Q$. Many standard texts indeed provide proofs that the points with this operation form a group.

Now, as you may have noticed, this way of defining the group depends very much on the way we represent the elliptic curve. That is, it assumes that we write $E$ as the set of solutions to $y^2=x^3+ax+b$. Can we also define the group law without making this assumption? The answer is yes.

How to do this, is quite complicated. Think of an elliptic curve $E$ as a very abstract object, not even assuming how to represent its points. It can be shown, that there exist some group attached to $E$, which is the degree-0 group of something called the Picard group. We denote it by $\operatorname{Pic}^0(E)$. Even more, it can be shown that there is a bijection between the points of $E$ and elements of $\operatorname{Pic}^0(E)$. Because $\operatorname{Pic}^0(E)$ is a group, so are the points on $E$. 

So, we know that the points on $E$ form a group. How do we compute it? Well, it depends on how we represent points on $E$. If we choose to write points as $(x,y)$, where $y^2=x^3+ax+b$, then it is the classical way. If we choose to write points on $E$ as $(u,v)$ where $u^2+v^2=1+du^2v^2$, then it is done in the way you described.

TLDR How do we prove that your $x_3$ and $y_3$ are correct? As above, we need to prove that they correspond to a point on $E$ such that it corresponds exactly to the group law defined by $\operatorname{Pic}^0(E)$. For this specific case, your best bet is the original paper or the cryptographic application paper. In particular I would look at section 3 of the latter paper.