Hello all, one may look for "minimal system of axioms" for ZFC (or any other theory) in the following (unusual) sense : say that a subset S of ZFC is "sufficient" if there is an explicit procedure that constructs a model of ZFC from any model of S. Thus, for example, ZF is sufficient since inside ZF we can construct Godel's universe L which is a model for ZFC. My questions : are minimal sufficient subsets of ZFC known? Is extensionality+infinity+(power set)+(separation scheme) sufficient?