$$
\begin{array}{ll}
     |\exists y \in \dot{x} \varphi(y)| &= \sup_{t}|t \in \dot{x} \wedge \varphi(t)|
     \\
     \\
     &= \sup_t |\varphi(t)||t \in \dot{x}|
     \\
     \\
     &= \sup_t |\varphi(t)|(\sup_{y \in dom(\dot{x})}|y=t|\dot{x}(y))
     \\
     \\
     &= \sup_t \sup_{y \in dom(\dot{x})}|\varphi(t)||y=t|\dot{x}(y)
     \\
     \\
     &= \sup_{y \in dom(\dot{x})} \sup_t (|\varphi(t)\wedge y=t|)\cdot \dot{x}(y)
     \\
     \\
     &= \sup_{y \in dom(\dot{x})} \dot{x}(y)|\varphi(y)|
\end{array}
$$ <wrap right>$\square$</wrap>