Sometimes, it is interesting to look at the theory of all first-order statements that are true in some second-order theory. When we do this with the naturals, it's called "true arithmetic"; when we do it with the reals (as a field) we have "real-closed fields", etc.
Does there exist a name for the same idea with $\text{ZFC}_2$? Would such a thing be a "true ZFC" or a "ZFC-closed set theory" or something like that? Is there hopefully a better name than "the first-order theory of second-order ZFC?"
Has this been studied and are there any interesting references on it?
I am also very curious what models of this theory would look like or if there is any interesting structure theorem regarding them. In particular, what properties do they have that models of first-order ZFC don't? Is the minimal model of this theory the same as the minimal model of first-order ZFC, for instance?