Let $M_X = (X, \mathcal{F}_X, \mu)$ be a D1158: Measure space.
Let $M_Y = (Y, \mathcal{F}_Y)$ be a D1108: Measurable space such that

(i)	$\phi : X \to Y$ is a D201: Measurable map from $M_X$ to $M_Y$
(ii)	\begin{equation} \phi_* \mu : \mathcal{F}_Y \to [0, \infty], \quad \phi_* \mu(E) = \mu(\phi^{-1} E) \end{equation}
(iii)	$f : Y \to [0, \infty]$ is a D313: Measurable function on $M_Y$

Let $E \in \mathcal{F}_Y$ and consider first the case where $f$ is an indicator function $I_E : Y \to \{ 0, 1 \}$. Applying results

(i)	R1242: Unsigned basic integral is compatible with measure
(ii)	R4613: Map composition with indicator function

we have \begin{equation} \int_Y I_E \, d \phi_* \mu = \phi_* \mu(E) = \mu(\phi^{-1} E) = \int_X I_{\phi^{-1} E} \, d \mu = \int_X (I_E \circ \phi) \, d \mu \end{equation} That is, the claim is true for measurable indicator functions. The full claim then follows by applying the principle of measure-theoretic induction. $\square$