Question: Let's take some theorem of ZFC, e.g.:
$$(1)\: \exists x \forall y ( y \notin x) $$
We can then choose a constant, denote it by '$\varnothing$' to get the following:
$$(2)\:\forall x (x\notin \varnothing) $$
My question is: what's the precise proof of (2) given (1)? Also, let the axioms of FOL be the ones from Geoffrey Hunter's Metalogic (axiom schemata QS1-7), plus the axioms of ZFC (though I think they're irrelevant). The only allowed rule of inference is modus ponens. 

P.S. I know that the question is ridiculous, and obviously the "jump" between (1) and (2) makes sense. The only thing that bugs me is that I can't justify this "jump" formally :)

Answer: 
It is a standard theorem about FOL that given a theory which entails a wff $\exists\_1x\varphi(x)$, then we can conservatively add a new constant $c$ to the language of the theory, together with the new axiom $\varphi(c)$. This is conservative in this sense that we will still be able to prove nothing in the language of the original theory which we couldn't prove before (even when we use the new constant to instantiate old universal axioms -- see Henning Makholm's important comment below). So there is a good sense in which the new constant just sprinkles onto the original theory some "syntactic sugar" (some nice notation that enables the medicine to go down more easily, by helping us to put things more snappily or more memorably) without at all changing the basic power of the theory.

That is all that is going on in the present case. Adding notation for the empty set is typically just adding syntactic sugar, which we are allowed to do because, once we know there is a set with no members, it is immediate that this is unique, so we have $\exists\_1x\forall y(y \notin x)$, and we can apply that mentioned standard theorem.
See the following [post](https://math.stackexchange.com/questions/672221/defining-new-symbols-abbreviations-in-first-order-logic).

Form George Tourlakis, *Lectures in Logic and Set Theory. Volume 2 : Set Theory*, page 122 :

"Let us recall the basics of introducing new function symbols [in first-order logic]. Suppose that we have the following:

> 
> $\vdash\_T (\exists y) A(y, x)$ --- [call it : "*existence* condition"]
> 
> 
> 

and

> 
> $\vdash\_T A(y, x) \land A(z, x) \rightarrow y = z$ --- [call it : "*uniqueness* condition"]
> 
> 
> 

then we may introduce a new function symbol, say $f\_A$, into the language of $T$ by the axiom

> 
> $f\_ A(x) = y \leftrightarrow A(y, x)$".
> 
> 
> 

Now, in $\mathsf {ZFC}$ we have the **Null Set** axiom :

> 
> $\exists y \lnot \exists x (x \in y)$
> 
> 
> 

i.e.

> 
> $\exists y \forall x (x \notin y)$.
> 
> 
> 

Since it is provable from this axiom and the **Extensionality** axiom that there is a unique such set, we may use the "technique" described above to introduce the notation '$\emptyset$’ to denote it.

In conclusion, it is **not** enough to prove "the existence" condition; you need also "the uniqueness" condition.