The real and deep meaning of quantifiers in first order logic and set theory (Before we start, I'm sorry if my english isn't the best, I'm not a native speaker.)
I'm trying to fully understand  the language and quantifiers of first order logic and set theory, and here's something that I'm completely struggling with in these days. 
By the axioms of first order logic (such as $\forall x(x=x)$), we know that $\forall y \exists x(x=y).$ The proof of this is quite simple. Knowing that $\forall x(x=x),$ assume that $\neg (\forall y \exists x(x=y)).$ Then we get: 
$$\exists y \nexists x (x=y)$$
so eliminating $\exists$, in particular $\nexists x(x=t)$ so $\forall x(x \neq t)$ and so $t \neq t$, which contradicts $\forall x(x=x)$ because $t=t.$ Thus: $$\forall y \exists x (x=y).$$
With this result we know that $\forall y \exists x (x=y)$. Talking about sets and the $\sf ZFC$ domain of discourse, we can eliminate $\forall$ and substitute the $y$ variable with a new term, but if I choose the universal set $U$ (the set such that $\forall x (x \in U)$), we get that $\exists x (x=U).$ The axiom of extensionality tells us that two sets $a$ and $b$ are equal if and only if a generic set $z$ is in $a$ if and only if $z$ is in $b$ to, that is $a= b \Leftrightarrow \forall z(z \in a \Leftrightarrow z \in b).$ Then I can say that $\exists x \forall z(z \in x \Leftrightarrow z \in U)$ but $z \in U$ is universally valid by the definition of the universal set $U$, so $\exists x \forall z(z \in x)$, that is to say that there exists a universal set (it doesn't matter if we call it $x$ or $U$, since the universal set is unic). But in set theory using the axiom of foundation (or simply separation), we know that the universal set doesn't exists, so $\nexists x \forall z(z \in x),$ which clearly contradicts $\exists x \forall z(z \in x).$
Is there something that I'm missing about this contradictory result?  Does
 the universal instantiation $\forall x(\psi (x)) \rightarrow \psi (t)$ require that the set that we are replacing in the formula already exists (this could be true, since the universal set $U$ doesn't exists) ?  And even if it's really like this, why does our first order language about quantifiers not provide a method to distinguish bewtween right and wrong substitutions?  When we are stating $\forall x(x \in U)$ are we already assuming that such a set $U$ exists?
Even more deeply, does the formula 
$$\exists x(x=y)$$ express the existence of $y$ ("there exists an $x$ equals to $y$")? Because if it really does, then $\forall y \exists x (x=y)$ says us that everything exists. Or are all this formulas (like $\exists x(x=y)$) saying that there exists something that is equal to some other thing and nothing else?
Thank you in advance for the help :D
 A: 
we know that $∀y∃x(x=y)$. Talking about sets and the $\mathsf {ZFC}$ domain of discourse, we can eliminate $∀$ and substitute the $y$ variable with a new term, but if I choose the universal set $U$...

But in order to have a term "naming" the universal set $U$, we need a proof in the theory $\mathsf {ZFC}$ that such a set exists, and we have not such a proof.

Does the universal instantiation $∀x(ψ(x)) → ψ(t)$ require that the set that we are replacing in the formula already exists ?

Yes, because the standard semantics of first-order languages requires that terms denote objects in the domain of the interpretation.
Thus, regarding set theory, in order to use terms denoting specific sets, we need a previous proof of their existence.
A: Here is a proof that God exists:

... OK, what is going on?!?
A couple of things:
First, the terms we use in our language need not denote what we intend them to denote. In fact, this theorem would be true in any domain with at least one object in it. If I interpret this result in a domain with myself as the only object, then the result is still true ... though we would need to specify that I would be 'god' ... and clearly I am not the God one might have envisioned upon first reading this proof.
Now, we could of course envision a domain where the God of our choice is an object of our domain, and where 'god' denotes that particular God. But that still does not prove the existence of God. All it shows is that for that particular domain it would be true that there is something equal to that God .. well, duh, that God equals that God!
So ... here is the second thing to keep in mind: in mathematics we can imagine any kind of domain with any kinds of objects. Mathematical existence simply means possible existence, i.e. free from contradictions. So, as long as the God of your choice is not free from contradictions, then it can possibly exist, and we can use logic and mathematics to prove things about it ... although the particular result as indicated by you, which states that for everything in any imagined domain there is something equal to it is not exactly very interesting: it immediately follows from the rather trivial result that everything is equal to itself.
Still you say, why can I prove the existence of the universal set $U$, when we know that $U$ is a concept that leads to a contradiction?  Well, going back to the first point: just because you are able to plug in $U$ does not mean that $U$ denotes the universal set.  Again, for a domain where I am the only object in it, $U$ would have to be me.
And second, when you do try to specify that $U$ is meant to denote the universal set .. well, then you are just imagining something that can't be: this cannot be used as a proper formal semantics for first-order logic.
In sum, the 'deep' meaning of quantifiers is that they quantify over some imagined domain. And, when you have a statement that is always true, like $\forall y \exists x \ x = y$, then you have found something that is true for all possible domains ... though as pointed out: nothing of much interest at all.
A: I believe your root confusion is believing that $\forall x (\psi(x))$ means that $\psi(x)$ is true for any conceivable object $x$. Rather it asserts that $\psi(x)$ is true for any object $x$ that exists in the domain of discourse. You need a separate existence proof for some particular $t$ before you can claim that $\psi(t)$ is proven.
So when you're working with ZFC and you applied the transformation $\forall x (\psi(x)) \rightarrow \psi(U)$, you are implicitly making the assumption that $U$ exists within ZFC. Given that assumption, of course you can prove that $U$ exists in ZFC.
There's no problem with the implication from $\exists x(x = y)$ that $y$ must exist; it's straightforward that if something exists which is equal to $y$, then $y$ exists! Rather your misstep was assuming that $\forall x (\psi(x))$ produces true statements when applied to objects do not exist.
The formula $\forall y \exists x (x = y)$ does not mean "for every conceivable $y$ there is some $x$ that exists and is equal to it, it means "for every $y$ that exists, there exists some $x$ that is equal to it".
A: You assume that there exists a universal set, then seem surprised that you can conclude that there exists a universal set from this assumption. If you just don't assume it in the first place, then the problem does not arise. 

Does the universal instantiation require that the set that we are replacing in the formula already exists? 

Yes. In particular, whatever we substitute in must be one of the things that we were quantifying over.

Even more deeply, does the formula $\exists x(x=y)$ express the existence of $y$ 

Yes, $y$ needs to exist for that to make sense.

Because if it really does, then $\forall y\exists x(x=y)$ says us that everything exists.

Yes. Specifically, it tells us that everything that exists, exists. This is not a particularly interesting or surprising result.
