 A formula like \(\forall X(Xx) \rightarrow (Px \wedge Qx)\) now follows from the combination of second-order universal instantiation and an instance of second-order comprehension: \(\exists X\forall x(Xx \leftrightarrow (Px \wedge Qx))\).[10]