Reasoning about finite sums Let $X$ denote a finite set, and $q:X \rightarrow \mathbb{R}$ denote a function. Then $$\sum_{x \in X}q(x) \in \mathbb{R}.$$ Now suppose we have a function $f : X \rightarrow Y$. Then we can use $f$ to break up the above sum as follows:
$$\sum_{x \in X}q(x) \overset{*}{=} \sum_{x \in X, y \in Y, y = f(x)} q(x) = \sum_{y \in Y}\sum_{x \in X, y = f(x)} q(x) = \sum_{y \in Y} \sum_{x \in f^{-1}(y)} q(x)$$
Seems legit, but to be honest, I don't really understand the $\overset{*}{=}$ step at a purely logical level; all I can say about it is: "Its obvious!"
So define $\Phi = (x \in X)$ and $\Psi = (x \in X \wedge y \in Y \wedge y=f(x))$. It would be nice if it were true that: $$(*)\qquad \forall x\forall y(\Phi \iff \Psi),$$ but that just isn't true.

Question. If not $(*)$, then what relationship between $\Phi$ and $\Psi$ allows us to deduce $$\sum_{\Phi} q(x) = \sum_{\Psi} q(x),$$
and why does it work?

Please don't remove the abstract algebra tag; the above question makes sense for $\mathbb{R}$ replaced by an arbitrary commutative monoid, and I'd like to see what that community has to say about the issue.
 A: The set $X$ and the graph of $\varphi$, that is:
$$G_\varphi=\{(x,y):x\in X \wedge y=\varphi(x)\}$$
have the same number of elements.
Furthermore, we can define
$$\bar q:G_\varphi\to \Bbb R$$
as
$$\bar q(x,y)=q(x)$$
and the bijection $g(x)=(x,\varphi(x))$ for $x\in X$.
Note that $\bar q=q\circ g^{-1}$.
and you can write
$$\sum_{x\in X}q(x)=\sum_{(x,y)\in G_\varphi}\bar q(x,y)=\sum_{(x,y)\in G_\varphi}q\circ g^{-1}(x,y)=\sum_{(x,y)\in G_\varphi}q(x)$$
A: In the context of showing that
$$
\sum_{x \in X}q(x) = \sum_{x \in X, y \in Y, y = f(x)} q(x),
$$
defining $\Phi$ as a formula over $x$ and $\Psi$ as a formula over $x$ and $y$ (in particular, using the formulas you have chosen), it actually would not be nice at all if
$\forall x\forall y(\Phi \iff \Psi).$
Suppose for example that $X$ and $Y$ both have cardinality $3$. Then  $\Phi = (x\in X)$ is true for $9$ distinct pairs $(x,y)$. So if $\Psi$ really is equivalent to  $\Phi$, then $\sum_{\Psi(x,y)} q(x)$ will sum $9$ values of $q(x)$, whereas we only wanted the sum of three values. 
The reason the first equation is true is that there is one value of $y$, and only one value of $y$, that satisfies $x\in X \land y \in Y \land y=f(x)$ for each value of $x$ that satisfies $x\in X$. Therefore we get exactly the same terms, and the same number of terms, when summing over all the pairs $(x,y)$ that satisfy $x\in X \land y \in Y \land y=f(x)$ as we do when summing over all $x$ that satisfy $x\in X$.
I prefer to get to the final result more directly, however. The sets $f^{-1}(y)$ for $y\in Y$ are a partition of $X$, so if we iterate through those sets, and within each set iterate over all the members of that set, we will "visit" each member of $X$ once (because the sets in a partition contain all members of the original set) and only once (because no two sets of a partition contain an element in common), which is exactly what we intend by summing over $x\in X$.
A: If $R$ is a binary relation between finite sets $X$ and $Y$, i.e. if $R \subseteq X \times Y$, then $R$ is finite, and, if $g: R \to \mathbb{R}$ is a function, then (by a theorem on partitioned sums in commutative monoids)
\begin{equation}
\tag{*}\label{fub}
\sum_{x \in X} \sum_{y \in R(x)} g(x, y) =
\sum_{xRy} g(x, y) =
\sum_{y \in Y} \sum_{x \in R^{-1}(y)} g(x, y).
\end{equation}
In particular, if $q: X \to \mathbb{R}$ is any function, then
$$
\sum_{x \in X} |R(x)| \cdot q(x) =
\sum_{xRy} q(x) =
\sum_{y \in Y} \sum_{x \in R^{-1}(y)} q(x).
$$
The 'baby Fubini theorem' \eqref{fub} which results from partitioning the set $R$ in two (basically symmetrical) ways is 'obviously' true, but its role here is disguised by the conjunction of two very special conditions:


*

*the value of the function being summed happens to depend on only one of its two arguments; and

*$R$ is a functional relation, so the factor $|R(x)|$ disappears, because it is equal to $1$ for all $x \in X$.
A: I don't have the technical expertise to do this answer justice, but here's my best attempt, a variant on ajotatxe's idea about equinumerosity:

Proposition.
If $$\forall x \in X( |\{\Gamma\}| = |\{\Delta\}|),$$ then $$\sum_{x \in X,\Gamma} q(x) = \sum_{x \in X,\Delta} q(x)$$

Okay, that's not very clear, but I'll explain with an example: taking $\Gamma$ as the empty string and $\Delta$ as the string $y \in Y : y =f(x),$ we obtain:

Special Case.
If $$\forall x \in X( |\{\}| = |\{y \in Y : y = f(x) \}|),$$ then $$\sum_{x \in X} q(x) = \sum_{x \in X,y \in Y : y=f(x)}q(x)$$

which in turn implies that $$\sum_{x \in X} q(x) = \sum_{x \in X,y \in Y : y=f(x)}q(x).$$
Seems to sort of work. Any thoughts, comments, or suggested improvements, guys?
