Power object of a subobject ($PY=\mathrm{Eq}(r,1_{PX})$)

For a monomorphism $Y\hookrightarrow X$ in a Cartesian category, intersect the universal membership relation on $X\times PX$ with $Y\times PX$. The resulting subobject is classified by $r:PX\to PX$, and $r^2=r$. The equalizer of $r$ and the identity represents precisely families of subobjects of $X$ contained in $Y$, hence is a power object for $Y$. This construction only requires the power object of $X$ and finite limits.