[tromp]

I found Johannes Riebel's thesis [1] an excellent introduction to the formalization of Zermelo Fraenkel-Set theory, complete with detailed examples of formal proofs.

[1] https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-unde...