Elementary existence proof in first order logic Please forgive my dullness but I just don't know how to - formally - show that $$\lbrace \forall x\ \phi(x), \exists x\ x = x \rbrace \vdash \exists x\ \phi(x)$$ for an arbitrary formula $\phi(x)$. It seems easy when there are individual constants: $$\forall x\ \phi(x)\vdash \phi(a) $$ $$\phi(a) \vdash \exists x\ \phi(x)$$ But when the language doesn't contain individual constants, and $\exists x\ x = x$ is all that I know?

Let $y$ be a variable not occuring at all in $\phi(x)$. Then we have $$\forall x\;\phi(x)\vdash\phi(y)$$ per _Universal Instantiation_ and then $$\phi(y)\vdash\exists x\;\phi(x)$$ (because $x$ does not occur in $\phi(y)$) per _Existential Generalization_.

How come we don't even need $\exists x\;x=x$? Well, the rules of inference already incorporate that our universe of discourse is nonempty (variables are not of type "pink unicorn").