The axiom of choice says that a choice function exists. Have you ever noticed that we never actually use the choice function. The implication is that the choice function is mapped over an infinite set of subsets. That application of the choice function is a parametrization of the weakset operator. (Nobody ever talks about a weakset operator.)

\forall f_{c} \exists f_{a} [f_{a} : B \subseteq {P A - \emptyset} \to C \subseteq A]

Subsets are not disjoint in general. We would not think that continuous intervals are made from discreate choices, but we mearge them so the choices never happened. I suggest that disjoint choice is preferable, as a formulation of an axiom, to countable choice when it can be used.

From my point of view existential axioms are built up like limits. Adding an existential axiom makes more statements true (Assuming that we are not interested in making axioms that don't do anything useful), but we cannot separate those statements from the ones that were true before.

We cannot formalize an exclusive form of existential axioms, but imagining what it would be like focuses our attention on what the axiom is for. It may seem ironic that in the case of what we cannot disprove, it is formal arguments that will lead us astray. Making asumptions unknowingly, we, unknowingly, ask questions that cannot be answered; impeding progress.