It all looks good, the only remark I have is that in 3.5a) it is unnecessary to use the axiom of pair on C because by the axiom of extensionality C=E. Note that what you have is correct, just not necessary.

On a related I am also working through Jech's book on set theory and it is awesome!