Hey, I'm feeling very shaky for some reason. I'd like to run a few things by you guys. I can do formal if needed, but I'm trying to build up a better model in my head in which I can eventually reason more flexibly and quickly without making mistakes. I'm starting from the beginning. This is ZF, no Choice yet. (Please pardon my sleepiness, if it shows.) Theorem 1. If C is a class of sets such that Union(C) is a set, then C is a set. I think Union(Power(C)) = C, but for some reason, I can't talk myself through it clearly. Power(C) puts the members of C inside of a set, grouping them in all the different ways (empty set included). Union() then just empties the members of those sets right back out and the duplicates don't count. Is that wrong? Just a hint is good. Oh, sorry, that's not the way that I meant to go, but that's good to know too. Rather, starting with Union(C), which has emptied the members from each member of C, Power(Union(C)) puts them back into sets, grouped in all the different ways. This is a set by Power axiom. If C is a subset of this set, then C is a set by Subset/Specification. The thing that hangs me up is that the author has left open whether there are individuals (urelements) in addition to sets. And individuals would not be members of Power(Union(C)), would they? Do you think that what I'm trying to do is beneficial at all? I am not trying to be sloppy. I'm trying to break free from a given formalism. I want better mental models.