 This is one important difference with respect to second-order quantification generally, since we are not automatically able derive every instance of second-order comprehension from the other quantificational axioms. On the other hand, a simple instance of existential generalization allows one to move from suitable formulas of the form \(A \leftrightarrow A\) to an instance of propositional comprehension of the form \(\exists p(p \leftrightarrow A)\). 