Equivalence relation on a proper class

We define cardinality as an equivalence relation on sets. But the class of all sets is not a set, so how do we do that? In particular, I'm interested in the proposition that equivalence classes form a partition of the initial set. It seems like it can be translated to cardinality, but I do not know how, at least in ZFC (and I don't even know ZFC :))


We can of course define cardinality as you say: Two sets are equipotent (or have the same cardinality) iff there is a bijection between them.

You can prove directly that this notion is reflexive, symmetric and transitive. For example, the last statement is: For any sets $A,B,C$, if there is a bijection from $A$ to $B$ and a bijection from $B$ to $C$, then there is a bijection from $A$ to $C$. Note that this does not require that we reference directly the collection of equivalence classes or even that we consider a single equivalence class as a given object. What I mean is: We can do all that we need to do without talking about proper classes or collections of proper classes.

What would be the statement corresponding to "the equivalence classes of an equivalence relation on a non-empty set form a partition of the set into non-empty subsets"? Simply the conjunction of the following two statements: 1. "Cardinality is defined for all sets", which simply means that given any two sets $A$ and $B$, the statement "$A$ and $B$ have the same cardinality" is meaningful, and is either true or false. But of course that is the case, since $A$ and $B$ have the same cardinality iff there is a bijection between them, this is the very definition. In fact, "$A$ and $B$ have the same cardinality" is simply a linguistic shortcut for "there is a bijection between $A$ and $B$". 2. "Given two sets $A$ and $B$, if there is a set $C$ such that $A$ and $C$ have the same cardinality and also $B$ and $C$ have the same cardinality, then so do $A$ and $B$." And this can be easily proved in the expected way.

All of this can be easily formalized in set theory (ZFC or even much weaker systems). Again, the point is that there is no need to directly argue about proper classes or collections of classes (but, if you want, then there are also appropriate set theories, such as MK, where this is possible).