Consider, in the first-order NGB theory of sets, the following axioms: $$\vdash\exists x\forall y(y\notin x)$$ and $$\vdash\forall y(y\notin\varnothing)$$
The second one defines the constant $\varnothing$. Moreover, from the second axiom we get the first by $\exists$I inference rule.
So my question is: we can replace axiom $$\vdash\exists x\forall y(y\notin x)$$ with $$\vdash\forall y(y\notin\varnothing)$$?
On
Yes, but we have to assume the individual constant $\emptyset$ as primitive in the language.
The way used e.g. into Mendelson's textbook [see 6th ed., 2015, page 231] is to formalize $\mathsf {NBG}$ in a f-o language with a single predicate letter $A^2_2$ (i.e. $\in$) but no function letter or individual constants.
There is a similar situation in f-o Peano arithmetic $\mathsf {PA}$: the usual presentation is with the individual constant $0$ as primitive and axiom: $\forall x \ (0 \ne S(x))$, but we can dispense withh $0$ and replace the above axiom with: $\exists z \forall x \ (z \ne S(x))$.
Well, you can only write that second sentence if you have a constant symbol for "$\emptyset$". Since the language of NBG is $\{\in\}$, this isn't technically a sentence you can write.
Now, you could make an argument that maybe we should add a constant symbol to the language - but clearly we don't need it (by the first formulation).
As a side note, we don't really need the axiom of emptyset - we can get the emptyset via separation applied to an arbitrary set via the formula "$x\not=x$" (this uses the fact that the semantics for first-order logic require the domain to be nonempty).