Lévy reflection theorem (source code)

= Lévy reflection theorem
{c}

For every finite collection $\Phi$ of <first-order formula>[first-order formulas], there are arbitrarily large <ordinal>[ordinals] $\alpha$ such that, for every $\varphi\in\Phi$ and all parameters in $V_\alpha$,
$$
V_\alpha\models\varphi
\quad\Longleftrightarrow\quad
V\models\varphi.
$$
The reflecting ordinals for $\Phi$ form a closed unbounded class.