I'm looking for a reference for the following result. It seems like it must be known, or follow quickly from something known, but I have not been able to find it in any of the textbooks I have.
Let $(\Omega, \mathcal F, \mathbb P)$ be a probability space. Let $\mathcal G$ be a sub-$\sigma$-field. Let $\mu$ be a regular conditional probability for $\mathbb P$ given $\mathcal G$. By this I mean that $\mu: \mathcal F \times \Omega \to [0,1]$ is a probability measure (denoted $\mu_\omega$) in its first argument, $\mathcal G$ measurable in its second argument and satsifies $$\int_G \mu_\omega(A)\mathbb P(d\omega) = \mathbb P(A \cap G)$$ for all $A \in \mathcal F$ and $G \in \mathcal G$. Let $X: \Omega \times \Omega \to \mathbb R$ be bounded and $\mathcal G \otimes \mathcal F$ measurable. Let $$EX(\omega) = \int X(\omega, v)\mu_\omega(dv).$$
Theorem. $EX$ is $\mathcal G$ measurable and $$\int EX(\omega)\mathbb P(d\omega) = \int X(\omega,\omega)\mathbb P(d\omega).$$
(I've cross-posted this at MathOverflow.)