How can I finish this proof of the existence of the empty set?

Question

I am trying to prove the existence of the empty set for self-study: $$\exists X\forall x(x\notin X)$$ I am trying to use the axiom schema of specification. $$∀Y∃X∀x(x∈X⟺(x∈Y∧φ(x)))$$ I am confused on argument #2 of the proof.

Note the following abbreviations:
$x\neq X\iff\neg x=X$ $x\notin X\iff\neg x\in X$

1. $\forall Y\exists X\forall x(x\in X\iff (x\in Y\land \phi(x)))$
   axiom schema of specification
2. $\forall Y\exists X\forall x(x\in X\iff (x\in Y\land x\neq x))$
   second-order logic? 1
3. $\exists X\forall x(x\in X\iff (x\in Y\land x\neq x))$
   universal instantiation Y/Y 2
4. $\forall x(x\in X\iff (x\in Y\land x\neq x))$
   existential instantiation X/X 3
5. $x\in X\iff (x\in Y\land x\neq x)$
   universal instantiation x/x 4
6. $x\in X\implies (x\in Y\land x\neq x)$
   biconditional elimination 5
7. $(x\in X\implies x\in Y)\land(x\in X\implies x\neq x)$
   distributivity of implication over conjunction 6
8. $x\in X\implies x\neq x$
   simplification (to second conjunct) 7
9. $\forall x(x=x)$
   reflexivity of equality
10. $x=x$
    universal instantiation x/x 9
11. $\neg x\neq x$
    double negation introduction 10
12. $x\notin X$
    modus tollendo tollens 8,11
13. $\forall x(x\notin X)$
    universal generalization 12
14. $\exists X\forall x(x\notin X)$
    existential generalization 13

I don't know how to go from an axiom schema to one specific formula.

What rule of inference can I use to complete the proof?

Do I need to study second-order logic to handle this axiom schema?