Q:

Formal proof for risk-neutral pricing formula

As you know, the key equation of risk neutral pricing is the following:
$$\exp^{-rt} S_t = E_Q[\exp^{-rT} S_T | \mathcal{F}_t]$$
That is, discounted prices are Q-martingales.
It makes real-sense for me from an economic point of view, but is there any "proof" of that?
I'm not sure my question makes real sense, and an answer could be "there is no need to prove anything, we create the RN measure such that this property holds"...
Is this sufficient to prove that, within this model, the risk-neutral measure exists?
EDIT:
Some answers might have been misled by my notation. 
Here is a new one:
$$\exp^{-rt} X_t = E_Q[\exp^{-rT} X_T | \mathcal{F}_t]$$
where $X_t$ can be any financial asset. For example, a binary option on an underlying stock $S$.
In order to price the option, you would start with this equation and develop the right-hand side to finally solve for $X_t$.
My key question: what allows me to write the initial equation assuming I have no information about the dynamics of the option or its underlying.

A:

Note first that this key equation is only assumed to hold true under some extra assumptions.  Typically those assumptions are taken to be about absence of arbitrage, though it is possible to weaken them somewhat if you are willing to consider portfolio arguments or collectively agreeable objective function.
Anyway, the argument is this: if all the risk can be arbitraged away, then the price of any contingent claim should be equal to its price under the risk-neutral measure Q.
The mathematical proof can be grasped most easily by the old-school arguments where one shows delta-hedges eliminating stochastic terms from the SDE.  More mathematically elegant arguments involving the Girsanov theorem and Feynman-Kac formula are less intuitive.

A:

You can find a simple proof in the discrete time case at http://kalx.net/ftapd.pdf. I'm not sure what you are trying to derive with your Ito calculus, but here is a rigourous derivation of the Black-Sholes/Merton PDE: http://kalx.net/dsS2011/bms.pdf. The Black-Scholes '73 derivation is not mathematically correct.
The modern approach does not use so called real-world measures.

A:

Since I did not get any comments to my latest update, and since I find it quite convincing, I hereby post my solution as an answer.

maybe I can prove that Q exists assuming a lognormal distribution of $S_t$.
Assuming $dS_t = \mu S_t dt + \sigma S_t dW_t$
By Itô, $d(e^{-rt} S_t) = -r e^{-rt} S_t dt + e^{-rt} S_t dS_t$.
Replacing with the definition of  $dS_t$, I get:
$d(e^{-rt} S_t) = e^{-rt} S_t [(\mu - r)dt + \sigma dW_t] = e^{-rt} S_t \sigma [\theta dt +  dW_t]$. (with $\theta=\frac{\mu-r}{\sigma}$)
By Girsanov, we know that there exists a measure s.t $dW_t = dW_t^* - \theta dt$
We thus get 
$d(e^{-rt} S_t) = e^{-rt} S_t \sigma [\theta dt +  dW_t] = e^{-rt} S_t \sigma dW_t^*$ which means that $e^{-rt} S_t$ is a Q-martingale. 

If you think it's incorrect, feel free to comment, or even better, to correct!
The thing that worries me is that I need to know the dynamics of the asset, and I think I shouldn't have to...

