Metamath set variable a set but not a set? Huh? In Metamath, "every set variable is a set" is a theorem.  What to make of a statement like "not exists x ( x not equal x )"?  This can be proved starting with "for all x ( x = x )", applying double negation, then quantifier negation.  In "not exists x ( x not equal x )", the set variable x is a set just because it is a set variable, but also it is not a set because of what the sentence says (and the sentence is a theorem).  Which view is right?  What should I make of this?
One difference I notice between the theorems named
vex
and nex
is that $x$ is a free variable in one but is a bound variable in the other.
Specifically, vex states that
$$ \vdash x \in V. $$
In this statement, $x$ is a free variable.
So I think a more careful statement of the theorem in mathematical English
might be, &quot;Every free set variable is a set.&quot;
Once you put a quantifier in front of a variable,
for example in $ \vdash \lnot \exists x \varphi, $
the variable becomes bound and the rules of the quantifier
govern what is possible.
In particular, when we use $\lnot \exists,$ saying that something
does not exist, many properties (or lack of properties) that
would cause trouble if the thing existed can no longer cause trouble.
So, for example, $x$ must be a set if there is any such thing as $x,$
but if there is no such thing, we can just as easily call it a set
and not a set at the same time.
I'm reminded of an old joke:

A customer in a butcher shop asks the price of roast beef, and on hearing the answer, complains:
&quot;Why is the price so high? The price is a dollar lower at the shop across the street.&quot;
&quot;Why don't you go buy your roast beef there, in that case?&quot;
&quot;I can't, they're all out of roast beef.&quot;
&quot;Well, if I were out of roast beef, I could lower my price by a dollar.&quot;

Perhaps someone with deeper insight into logical notation
can explain the meaning of the variables in the
vex and nex theorems further.
You have actually recognized the problem introduced by Russell's paradox that motivates some set theorists to study set theory in terms of a modal structure obtained by its many possible models.  The problem is the distinction between what a quantifier is "supposed to mean" and how Russell's paradox interferes with the representation of classical quantifiers in the square of opposition.

If you examine the formal sentences associated with the square of opposition in the link,

https://plato.stanford.edu/entries/square/#ModRevSqu

you can see the problem with "Every set is not an element of itself" and interpreting the universal quantifier in terms of sets.  Free variables carry implicit universal quantification on the basis of what quantifiers are "supposed to mean".

It is best to remember that metamath is intended to execute logical transformations.  So, you may view the system as either assuming that set theory has a model or that it is treating set theory in a purely formal matter.

If you would like to consider the problem of negative existentials further, 
look at the link,

https://plato.stanford.edu/entries/existence/#FreRusExiNotProInd