Suppose we have a class equivalence relation ~ on a proper class C. Can we form the class of equivalence classes C/~? What axioms do we need, assuming we base ourself on NBG? I can't seem to prove that this class exists with the axioms stated. I.e., the proposition that there exists a class D, and a surjective class function F : C -> D such that x ~ y if and only if F(x) = F(y). Axiom of global choice doesn't work here either. A single equivalence class may be a proper class, and since this axiom only applies to the class of sets (and not a "collection" of classes), we may not pick out a single representative this way. Formally the equivalence relation is a subclass of the cartesian product CxC satisfying the necessary conditions. The cartesian product exists by the axiom of pairing, and the axiom of unrestricted comprehension. Take a look at the wikipedia entry for quotient categories. The way it is worded, it seems to imply that the quotient category may always be constructed given a categorical equivalence relation on a category. Consider the category consisting of a single object X, with morphisms being simply the class of sets. Composition is defined as union (clearly associative). The identity morphism is the empty-set. Define an equivalence relation on hom(X,X) by x ~ y if x and y are in bijection. This clearly defines a congruence relation as described in the link. However, the quotient category would be the category of a single object, with morphisms corresponding to cardinal numbers. As a category, the morphisms should form a class. However, assuming that quotient categories always exists, this seems to imply that we have constructed the class of cardinal numbers. So how is this this construction defined? Clearly, if the category is locally small this may be done using the global choice function. The trouble appears when dealing with not locally small categories.