In the article Generalization in ZF [HTML]
I formally define the notion of generalization in ZF set theory.
I also formalized the results of that article in the form of Isabelle proof assistant source files. You can download [HTML] the Isabelle files.