Defining the pair $(A,B)$ in $\mathsf{ZFC}$ where $A,B$ are classes In $\mathsf{ZFC}$ a class $C$ is defined by a formula $\phi(x)$: conceptually $C = \{ x : \phi(x) \}$, and if $a$ is in $C$ we mean $\phi(a)$. 
If $A$ and $B$ are two classes, how does one define the pair $(A,B)$?
P.S. In theory of categories we have the pair $(\operatorname{Obj},\operatorname{Mor})$ where $\operatorname{Obj}$ and $\operatorname{Mor}$ are classes (objects and morphisms, respectively) then I wonder how to define this pair in $\mathsf{ZFC}$.
 A: Strictly speaking, you can't form the ordered pair $(A,B)$ using the standard definition (Kuratowski's) if either $A$ or $B$ is a proper class, because it requires $\{A,B\}$ to exist, and this in turn implies that both $A$ and $B$ are sets. For example, there is no entity (V,Ord)(V,Ord). The standard definition of the pairing function increases rank, where the rank of a set $x$ is the least ordinal $\alpha$ such that $x\in V_{\alpha}$, and $V = \bigcup_{\alpha\in Ord} V_{\alpha}$ where $V$ is the universe of set theory.
A standard workaround in category theory is to assume that you're working within a set model of ZFC — say, $V_{\kappa}$ for some inaccessible cardinal ${\kappa}$. Then $\rm Obj$ and $\rm Mor$ are proper classes of the model, but sets in the true universe, where $(\rm{Obj}, \rm{Mor})$ exists and is just the usual ordered pair. Note that any such $V_{\kappa}$ is more than big enough to contain the true versions of every entity used by (say) 95% of mathematicians, and has enough closure to contain their constructions.
Tarski's Axiom aka the Axiom of Universes, which category theorists and algebraic geometers like, says that every set is a member of some Grothendieck universe, a larger set which is a model of set theory. It basically asserts that there are unboundedly many inaccessibles, and guarantees that you always have enough headroom. So it's really a (fairly modest) large-cardinal axiom.
A couple of other solutions: 


*

*Let (A,B) be a/the disjoint union of A and B — say, $\{0\}\times A \cup \{1\}\times B$ — and define projection functions appropriately. 

*Use a flat pairing function, which doesn't increase rank. See e.g. https://mathoverflow.net/a/62801 for Quine's definition, which works on proper classes too.

