  It can then be checked that all the usual axioms of set theory extensionality, power set, union, comprehension over bounded formulae (and even antifoundation, so that the membership relation does not need to be well-founded) hold in this simple model. (A bounded formula is a formula where all quantifications are of the form \(\forall x \in a\ldots\) or \(\exists x \in a\ldots\)). In this way it can been shown that Church’s simple type theory is equiconsistent with the bounded version of Zermelo’s set theory.