This subsection gives a definition of an ordered pair, or couple (2-tuple), that "works" for proper classes, as evidenced by Theorems bj-2uplth and bj-2uplex, and more importantly, bj-pr21val and bj-pr22val. In particular, one can define well-behaved tuples of classes. Classes in ZF(C) are only virtual, and in particular they cannot be quantified over. Theorem bj-2uplex has advantages: in view of df-br, several sethood antecedents could be removed from existing theorems. For instance, relsnopg (resp. relsnop) would hold without antecedents (resp. hypotheses) thanks to relsnb). Also, the antecedent could be removed from brrelex12 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct could be simplified by removing the exception currently made for the empty set.
The projections are denoted by and and the couple with projections (or coordinates) and is denoted by .
Note that this definition uses the Kuratowski definition (df-op) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg) without needing the axiom of regularity; it could even bypass this definition by "inlining" it.
This definition is due to Anthony Morse and is expounded (with idiosyncratic notation) in
Anthony P. Morse, A Theory of Sets, Academic Press, 1965 (second edition 1986).
Note that this extends in a natural way to tuples.
A variation of this definition is justified in opthprc, but here we use "tagged versions" of the factors (see df-bj-tag) so that an m-tuple can equal an n-tuple only when m = n (and the projections are the same).
A comparison of the different definitions of tuples (strangely not mentioning Morse's), is given in
Dominic McCarty and Dana Scott, Reconsidering ordered pairs, Bull. Symbolic Logic, Volume 14, Issue 3 (Sept. 2008), 379--397.
where a recursive definition of tuples is given that avoids the 2-step definition of tuples and that can be adapted to various set theories.
Finally, another survey is
Akihiro Kanamori, The empty set, the singleton, and the ordered pair, Bull. Symbolic Logic, Volume 9, Number 3 (Sept. 2003), 273--298. (available at http://math.bu.edu/people/aki/8.pdf)