Bounded formula in set theory (${\Delta }_0$)

A bounded formula in set theory has every quantifier in one of the forms $\forall x\in y$ or $\exists x\in y$. Such formulas are absolute between transitive models containing their parameters.

A first-order formula is ZF-equivalent bounded if ZF proves it equivalent, with the same free variables, to a syntactically bounded formula in set theory. It need not itself have only bounded quantifiers. Between transitive models of ZF, use the bounded equivalent and the axioms in each model to prove set-theoretic absoluteness. The syntactic bounded-formula result requires only transitivity; the provable-equivalence extension additionally requires the theory used for the equivalence.