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 :)