If we restrict all parameters in the set building axioms of $\sf ZFC$ to definable sets, would the celebrated Cantor's theorem still apply? Can existence of uncountable sets be proven at all?
The set building axioms of $\sf ZFC$ are the axioms of: pairing, union, powerset, Separation and Replacement\Collection.
To clarify what I mean by this restriction, the idea is that the parameters to be definable by formulas having a single free variable, take the axiom of pairing for example, this would turn into the following scheme:
Pairing: if $\varphi; \psi$ are formulas in which "$x$" only occurs free, and that do not have a free variable other than "$x$"; then:
$\forall a \forall b \, \bigl(a=\{x \mid \varphi\} \land b=\{x \mid \psi \} \\\to \exists c \forall y \, (y \in c \leftrightarrow y=a \lor y=b )\bigr)$
In other words, is it consistent to add an axiom that all sets are countable?