We show that there have been common ideas concerning "safety" properties of first-order formulas which were independently developed in set theory, in computability theory and Metamathematics, and in database theory. We develop a general unified framework for dealing with safety issues, based on a generalization of the notion of a first-order signature, and demonstrate its usefulness in all these areas. In the case of set theory it leads to a new formalization of the axiomatic set theory ZF which reflects real mathematical practice, and is easy for mechanical manipulation and interactive theorem proving. Unlike the standard first-order formalizations, this version provides a rich class of abstraction terms denoting sets on the one hand, and is based on purely syntactical (rather than semantic) considerations on the other hand.