I've seen the following statement a few times:

"Let $A$ be a set, then $\emptyset\subseteq A$".

Or, written 'more formally': $$ \forall A\,\, \emptyset\subseteq A $$

My doubt is: I've always seen the quantifier $\forall x$ to mean "for all $x$ elements of some set $S$". However, when talking about all the sets, how do we define this quantification?


It's just an unbounded quantifier, not constrained to the elements of a fixed set $S$. This is the normal case; the bounded quantifiers, constrained to members of a set, are defined in terms of the basic quantifiers, $\forall x$ and $\exists x$.

$\forall x$ means just that: for all $x$, anything $x$. In the mathematical universe, $x$ ranges over sets, and not, say, people, atoms, oranges, etc. Unless some further conventions are in force constraining $x$ to range over, for example, only reals, $\forall x$ means "for all sets $x$". In order to say "for all $x$ in $S$" you have to bound the quantifier, as in "$\forall x\in S$". However, bounded quantifiers are a shorthand, defined in terms of the basic unbounded quantifiers: $$\begin{align} \exists x\in S\,P(x) &\stackrel{def}\iff \exists x\,(x\in S \land P(x)) \\ \forall x\in S\,P(x) &\stackrel{def}\iff \forall x\,(x\in S \to P(x)). \\ \end{align}$$


From the ZFC perspective, there's nothing special going on here. In ZFC, everything is a set, and universal quantification is always regarded as quantification over the entire world of sets (the "cumulative hierarchy"). So the sentence $\forall x P(x)$ always means "for all sets $x$, $P(x)$." By convention, the notation $\forall x \in X, P(x)$ is viewed as a convenient shorthand for the more cumbersome $\forall x(x \in X \rightarrow P(x)).$

On the other hand, from the type-theoretic perspective, this is an example of "quantification over type variables," and it is usually treated separately to ordinary quantification. I suggest using Google to learn more.