 Pi-one formula modulo ZF

A first-order formula is ${\Pi }_1^{\mathrm{ZF}}$ if ZF proves it equivalent, with the same free variables, to a universal unbounded quantifier block followed by a bounded formula in set theory. Bounded quantifiers do not increase its level in the Lévy hierarchy. Such properties are downward absolute between appropriate transitive models of ZF.