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: 
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.
Let's add my rather informal view:

I think the definitions are considered only some kind of meta thing and not actually part of the language.

So you have to choose a way to give a meaning to definitions.

I can think of 2 kinds of definitions:

* A property. Let's say $x$ is not empty means $\exists y(y\in x)$
* An object. You want to denote the $\varnothing$ the $x$ such that $x$ is not empty.

Now let's try to resolve the following formula
$$\forall x(x\text{ is not empty}\Longrightarrow x\ne\varnothing)$$

It's quite clear how to resolve a property, it's equivalent to
$$\forall x(\exists y(y\in x)\Longrightarrow x\ne\varnothing)$$
but what about $\varnothing$? One way to look at it is to say the formula holds for all $x$ ($z$ in this case) from the definition of $\varnothing$
$$\forall z(\exists y(y\in z)\Longrightarrow\forall x(\exists y(y\in x)\Longrightarrow x\ne z))$$
For this to be actually useful, you need to known such $z$ exists and that it's unique. Both are quaranteed if $\varnothing$ is well defined.