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.