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.