Why bother proving that a class is a set? Fix a set theory, say ZFC. Now suppose you have a statement $P(x)$ written in the language of that theory, which has precisely one free variable $x$. We can conceive of the class of all $x$ in the domain of discourse such that the statement $P(x)$ holds. It is my understanding that this class may or may not itself correspond to an object in the domain of discourse. My questions are as follows. Firstly, suppose that it does correspond to an object in the domain of discourse, well what do we gain by proving that this is the case? And secondly, if the class of all such objects does not correspond to an object in our domain of discourse, what are we NOT allowed to do with this class which we would perhaps like to be able to do?
Now firstly, let me apologize in advance if my conceptualization above is either imprecise, or founded on false assumptions. My experience is limited to naive set theory, and I have no model theory under my belt.
Secondly, let me provide some background context for my question.
Suppose I have a unary function $f$ and I want to speak of the set of all sets that are closed with respect to $f$. We might write this as $\mathrm{clo}(f)$. My understanding is that even if $\mathrm{clo}(f)$ is defined only on 'small' functions $f$ (that is, those functions that are defined by a set of ordered pairs), nonetheless $\mathrm{clo}$ is going to be 'big'. Is this going to be a problem?
Now things get messier. I want to define a binary function $\curvearrowright$ such that for any object in the domain of discourse $x$ and any function $f$, we may write that $x \curvearrowright f = f(x)$. However, I don't want to limit this to small functions $f$. For instance, letting the object $x$ be replaced by a small function $g$, and letting $f$ be replaced by the large function $\mathrm{clo}$, I want to be able to write $g \curvearrowright \mathrm{clo}$ for the set of all sets that are closed with respect to $g$. Can this be done without introducing contradiction?
 A: Well, let us assume we are working in ZFC. In this case:


*

*We are not allowed to quantify over classes which are not sets.

*We cannot collect proper classes into other classes.

*We cannot say that a class "exists".

*We cannot use classes as parameters internally.


One of the main uses of set theory is to give a foundation to the rest of mathematics. If you cannot say that an object exists in your foundation, how can you delegate it to other theories? You can't. You can only talk about it as a syntactical construct, without any semantical meaning.
If you want to define the class $\operatorname{clo}(f)$ and $f$ itself is a class then your definition is not within the theory. Of course if you are not a set theorist it will probably interest you as much as it would interest you to know that I'm hungry right now. You should know, and you probably do, that there are ways around it like class-set theories or large cardinals.
Furthermore, if you define the operation for class functions and you want to talk about the collection of "all functions which have such and such closure" then you can only do that if these functions form a set. You cannot talk about a collection of classes, not in ZFC and not in NBG. You need to go another step to allow $2$-classes (classes of classes).
This form of iteration can go on for a while before it settles down and you find yourself with a large cardinal. It is somewhat necessary for some constructs in categories, but it is not always necessary otherwise. 
Your $\curvearrowright$ function takes input of a function and a set. If the function is not a set, then $\curvearrowright$ cannot take it as input.
A: One thing that you can do with a set is put a poset structure on it and use Zorn's Lemma, which is a very powerful technique in proving the existence of certain objects. The following is a false application of Zorn's Lemma that illustrates its usefulness and the necessity of proving set-hood. 
Suppose you want to prove that any field $F$ has an algebraic closure. Consider the collection of all algebraic extensions of $F$ and order this collection by inclusion. It is easily seen that all of the conditions for Zorn's Lemma hold and that a maximal element is an algebraic closure. The only problem is that the collection is not a set and thus this proof is wrong. It can be corrected but it requires a bit more work to actually produce a set.
Now, the following example shows that a very similar variant of the 'proof' above can be construed that 'proves' nonsense. Consider now the collection of all sets and order it by inclusion. Again, the conditions of Zorn's Lemma are easily satisfied and a maximal element now gives us a set with the property that it is not properly contained in any other set, obviously nonsense. 
Another thing one can do with a set is use it to index other sets and then take the cartesian product of the indexed family. If one instead uses a proper class to index some sets then the cartesian product may or may not exist and determining if exists or not can be very difficult. This type of importance in distinguishing between sets and proper classes is very general. Indeed, given any small category it is well known that if the category admits arbitrary (i.e., class indexed and not just set indexed) categorical products (of which the cartesian product of sets is a special case) then the category degenerates to a poset. This argument thus shows that in any category which is not a poset (the category of sets is an example of a non-poset category) there must exist a proper class indexed family of sets which has no product in the category. In contrast, many categories (that of sets included) have the property that any set indexed family of objects has a product in the category (more generally, all small limits and colimits exist in many categories but if all limits, or all colimits, exist then the category must be a poset). 
