Integration formula for the product measure

Let $(X,\mathcal F,\phi)$ and $(Y,\mathcal G,\psi)$ be two probability spaces and $(Z,\mathcal H,\mu)$ be their product space: i.e. we have that $Z = X\times Y$. Given an arbitrary set $F\in\mathcal H$ and any point $x\in X$ let us define $$\pi_x(F) = \{y\in Y:(x,y)\in F\}.$$ I wonder if the following formula is true: $$\mu(F) = \int\limits_X \psi(\pi_x(F))\phi(dx).\tag{1}$$

I think it is true and the proof goes like this:

1. For any $A\in \mathcal F$ and $B\in\mathcal G$ we have $$\int\limits_X \psi(\pi_x(A\times B))\phi(dx) = \int\limits_X \psi(B)1_A(x)\phi(dx) = \phi(A)\psi(B) = \mu(A\times B)$$ so $(1)$ is true for the class $\mathcal C$ of measurable rectangles $A\times B$.

2. If $(1)$ holds for $F\in \mathcal H$ it also holds for $F^c$.

3. If $(1)$ holds for the disjoint sequence $(F_n)_{n\geq 0}$ in $\mathcal H$ then it holds for $F = \bigcup\limits_{n\geq 0}F_n$.

As a result, if $\mathcal H'$ is the class of sets for which $(1)$ holds then $\mathcal C\subset \mathcal H'$ and it is closed under taking complements and countable unions, so $\mathcal H'$ is a $\sigma$-algebra and hence $\mathcal H\subset \mathcal H'$ hence $(1)$ is true for any $F\in \mathcal H$.

My question are the following: first, please tell me if the proof is correct, especially I am not sure if I need to show measurability of $\psi(\pi_x(F))$ or is it implicitly proved already. Second, if the result is true I'm pretty sure it is known - so I wonder about a reference.

-
That is the Fubini Theorem, see for example Real Analysis by Stein and Sakarchi! – checkmath Apr 17 '12 at 11:01
You can also check Measures, Integrals and Martingales by R. L. Schilling page 123. – Stefan Hansen Apr 17 '12 at 11:45
@chessmath: thanks for the reference, but I was rather looking for the general result, not related to $\mathbb R^n$ and Lebesgue measure – Ilya Apr 17 '12 at 13:18

In order for (1) to well-defined you need to show that $x\mapsto \psi(\pi_x(F))$ is $(\mathcal{F},\mathcal{B}(\mathbb{R}))$-measureable for all $F\in \mathcal{H}$. You can do this the following way:
• Convince yourself that $\pi_x(F)\in \mathcal{G}$ for all $F\in \mathcal{H}$ and $x\in X$.
• Define $\mathcal{D}=\{H\in \mathcal{H}\mid x\mapsto \psi(\pi_x(H)) \text{ is measureable}\}$ and show that this is a Dynkin-system, which contains $\{F\times G\mid F\in\mathcal{F},\, G\in\mathcal{G}\}$.
• Use Dynkin's Lemma to conclude that $\mathcal{D}=\mathcal{H}$.