(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