ZF

Gödel's model is an example of a simple type of inner model that might be called a definable transitive inner model³), where the universe is replaced by a transitive subuniverse defined within ZF, the membership relation is just the original one restricted to the subuniverse, and where the axioms of ZF relativized to the subuniverse, are provable within ZF.