Wilfried Sieg and Patrick Walsh wrote a paper detailing the formal development of set theory in a conceptual way in this paper. See in particular sections 3 and 4.
The intractive proof program used in the construction of formal proofs is called ProofLab and its automated checker is AProS. It is currently written in Java, which throws some security flags from operating systems and browsers. Please change your security settings if you wish to use the Lab. It is transitioning to an HTML version currently, and we will update this page when that is complete.
Beyond the description given in the paper, there are syntactic considerations that occur in the construction of proofs. We have therefore created a manual for reference.
Collected here are the formal proofs using the ProofLab. This is only a preliminary presentation of the proofs. Check back here later for more explanation, elaboration, and organization.