Implication details

Proof: This follows from the fact that for an elementary topos $\T$, the power object functor $P : \T^{\op} \to \T$ is monadic (Johnstone, 2.2.7), and therefore creates limits (i.e. it creates colimits in $\T$ from limits in $\T$).