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?

Clarification: by parameters in the abovementioned set building axioms, I mean the variables quantified before the asserted to exist set.

One more remark, I noticed that there can be many versions of this question by easing those restrictions from some of the mentioned axioms. One version is to just remove that restriction from pairing, or just remove it from powerset axiom, or actually just remove it from both pairing and powerset axioms. We can also have similar partial easing with any of union or powerset, or any two of pairing, union, and powerset. I think most interesting would be to limit definability of parameters to axioms of Set Union, Separation and Replacement\Collection.

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?

Clarification: by parameters in the abovementioned set building axioms, I mean the variables quantified before [i.e., on the left of] the asserted to exist set.

One more remark, I noticed that there can be many versions of this question by easing those restrictions from some of the mentioned axioms. One version is to just remove that restriction from pairing, or just remove it from powerset axiom, or actually just remove it from both pairing and powerset axioms. We can also have similar partial easing with any of union or powerset, or any two of pairing, union, and powerset.

I think most interesting would be to limit definability of parameters to axioms of Set Union, Separation and Replacement\Collection.

An even less restrictive version is to just limit the condition of definability of parameters (in the above sense) to the instances of Separation and Replacement\Collection.

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?

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?

Clarification: by parameters in the abovementioned set building axioms, I mean the variables quantified before the asserted to exist set.

One more remark, I noticed that there can be many versions of this question by easing those restrictions from some of the mentioned axioms. One version is to just remove that restriction from pairing, or just remove it from powerset axiom, or actually just remove it from both pairing and powerset axioms. We can also have similar partial easing with any of union or powerset, or any two of pairing, union, and powerset. I think most interesting would be to limit definability of parameters to axioms of Set Union, Separation and Replacement\Collection.