 Lévy reflection theorem

For every finite collection $\Phi$ of first-order formulas, there are arbitrarily large ordinals $\alpha$ such that, for every $\phi \in \Phi$ and all parameters in $V_{\alpha }$,There is a closed unbounded class of ordinals reflecting every formula in $\Phi$; one obtains such a class after closing the finite list under subformulas.