Is it possible to avoid redundancy in a foundational work? Imagine we're developing all of mathematics from scratch. We settle on using a set-theoretic foundation.
Early on, we assert that an ordered pair $(x,y)$ can be abbreviated $xy$ whenever there is no ambiguity, and we define that a relation is a set of ordered pairs (alternatively, a subset of a Cartesian product). Furthermore, for any relation $f$, we define that $f\langle X \rangle = \{y \,|\,\exists x \in X : xy \in f\}$. We go on to prove the proposition that $f\langle X \cup Y \rangle = f\langle X \rangle \cup f\langle Y \rangle$.
A little later in the piece, we're looking at powersets and related ideas. We define that $\beta$ denotes the inclusion relation (a proper class). So $\beta^{-1}\langle \{Y\}\rangle$ denotes the powerset of $Y$. Symbolically, $\beta^{-1}\langle \{Y\}\rangle = \mathcal{P}(Y)$. And it follows easily that $\beta^{-1}\langle \{Y,Z\} \rangle = \mathcal{P}(Y) \cup \mathcal{P}(Z)$, by our proposition.
However, the above paragraph is bogus. The expression $\beta^{-1}\langle \{Y\}\rangle$ needn't denote the powerset of $Y$, because we haven't defined the meaning of this expression in the case where $\beta^{-1}$ is a proper class. Thus, we have to include "redundant" definition. To make things worse, our proposition was only proved for all relations, which doesn't include proper class relations. So now we need a "redundant" proposition (we copy-and-paste the proof!).
Clearly, this is very silly. Now the obvious solution is to have allowed relations to be proper classes in the first place. But this just pushes the problem up; now, it is relations between proper classes that our proposition has missed. Thus, we still have to deal with redundancy. My question is, how can we make sure our definitions/propositions don't need to be "doubled up".
 A: You run into a problem because you want something that would work both for classes and sets, but in $\mathsf{ZFC}$ there is a huge difference between classes and sets. The latter is an object whereas the former might not be an actual object of the universe.
One way out is to talk about "collections" without specifying whether this is a class or a set, but this is not fully accurate because there is no well-defined notion of a collection. For example one can talk about the collection of all classes, but this collection is neither a set nor a class. It's a metatheoretical, or perhaps metamathematical notion.
Another way is to define things schematically in a similar way to the way we write the replacement schema. Whenever a formula defines something such and such then it is a relation. But this too amounts to arguments in the metatheory, because now we can't really say "Any well-ordered relation on $\omega$ has an initial segment isomorphic to $\langle\omega,\in\rangle$". Because this is a statement about all relations, but relations are no longer collections of ordered pairs -- they are definable collections. So this is a proof in the metatheory going over all the formulas.
(It is possible that there is a way to overcome this difficulty and write a formula which automatically generates relations over a particular set, without an appeal to a metatheoretical argument, but I don't see one right now.)
So we are again stuck. There is another way out, simply use a theory whose spectrum includes classes. Something like $\mathsf{NBG}$ which is a conservative extension of $\mathsf{ZFC}$ (it does not prove new theorems about sets), and allows classes. One can also consider to use the Tarski-Grothendieck set theory with universes, which is roughly the same as $\mathsf{ZFC}$+"there is a proper class of inaccessible cardinals". This allows us to treat classes as sets of another universe so the definitions go smoothly, but do note that the consistency strength of this theory is stronger than just using $\mathsf{ZFC}$.
Lastly, one can decide to use modern approaches to foundations like type theory based approaches, e.g. $\mathsf{SEAR}$, or other structural set theories such as $\mathsf{ETCS}$. Those might be prone to problems of their own, but I cannot really say what these problems might be due to a lack of knowledge on the topic.
From the meta-mathematical point I should add that we don't often write concrete proofs. We write schemata of proofs. Every time we say an ordered pair we don't really talk about $\{\{a\},\{a,b\}\}$. We actually say "fix $\varphi_p(x,y,z)$ which states that $z$ has the properties required from the ordered pair $\langle x,y\rangle$..." then every time you refer to ordered pairs you refer to this formula. But this is not really dependent in the actual formula. 
Similarly for functions we can require different definitions, and the process goes the same. Of course we often take the union of functions, but we can redefine this operation just as well - and everything works as before, even if it is now somewhat cumbersome.
In this aspect there is no reason to expect a proper proof of "lack of redundancy", and when we talk about class relations we often treat the proofs schematically. We know the proof works because the relations have the wanted properties, and then we don't really care anymore.
As the final line implies, we have to verify that the relation we intend to use have the properties which fit into the schema we intend to use. For example well-foundedness or set-like properties.

Further reading:


*

*difference between class, set , family and collection

*Difference between a class and a set

*What can I do with proper classes?
