Universal Objects in Big Categories

Let $\mathcal{A}$ be a category whose collection of object forms a proper class. Then, to be able to formulate the concept of a terminal object in $\mathcal{A}$, do we have to leave ZFC? In other words, can we formulate the concept of a terminal object in $\mathcal{A}$ inside ZFC. If yes, how could we do it?

For example, in the category $\mathcal{Sets}$ of all sets. A singleton is a terminal object in $\mathcal{Sets}$, which could be checked by hand. But if we want to actually define what a terminal object is, then we have to quantify over all Sets, which is not a set. So, the definition is ill-formed inside ZFC?

A similar issue arises when we talk about things like injective objects, projective objects etc. of an arbitrary abelian category. How do we resolve this?

(I must be very confused about this basic issue; any help to resolve this will be greatly appreciated)

EDIT 1: What happens if in $\mathcal{A}$, $\hom(A,B)$ may also be proper classes where $A$ and $B$ are arbitrary objects of $\mathcal{A}$?

-
In first-order logic, you can quantify over all objects of the given theory (in this case, ZFC). There is no reason whatsoever why quantification should be restricted to a set. That’s a basic principle of first-order logic. –  Emil Jeřábek May 5 '11 at 15:14
That is, $t$ is a terminal object iff it satisfies the formula $(\forall u)(O(u)\to(\exists!f)H(f,u,t))$, where $O(x)$ and $H(f,x,y)$ are formulas defining the classes of objects and morphisms of $\mathcal A$, respectively. –  Emil Jeřábek May 5 '11 at 15:27
Thanks a lot! How about when the collection of arrows are also proper classes? (See EDIT 1 above). –  QcH May 5 '11 at 17:38
This does not make any difference. Judging from your comment below, your worry is about the $\exists!$ quantifier. However, $\exists!x\,A(x)$ is a short hand for $\exists x\,\forall y\,(A(y)\leftrightarrow x=y)$ (or something equivalent), it does not involve the cardinality of any sets (or classes). –  Emil Jeřábek May 5 '11 at 17:47
@Qph: I just saw your edit. Why should anything change? The treatment given in the answer by Emil or by me is the same whether or not $\hom(A, B)$ is small or not. (As mentioned in these answers, a class in ZFC is given by [is informally the extension of] an unary predicate written in ZFC, and thus you can manipulate them as you do predicates. Insofar as they may not be sets, some set-theoretic constructions like power sets may not be applicable to them, but nothing like that applies to your question.) –  Todd Trimble May 5 '11 at 17:52

In ZFC, a class is given by a class formula $\phi$, that is, a formula expressed in the language of ZFC. For example, the notion of group can be formalized by such a formula $\phi$. The notion of group homomorphism can also be so formalized, say by $\psi$. So in principle there is no problem in being able to write down a formula in ZFC whose abbreviation is

$$\exists 1 \ \forall G \ \phi(G) \Rightarrow \exists ! f \ \psi(f) \wedge dom(f) = G \wedge cod(f) = 1$$

and this is what you're after.

"Unbounded" quantification takes place all the time in ZFC. For example, the pairing axiom involves the formation of a set $\{x, y\}$ for any two sets $x, y$, and this "any" involves quantification over the class of sets. The axioms of set theory should be formulated to avoid completely unbounded instances of say the comprehension or separation axiom, as we know from the classical set-theoretic paradoxes, but all this is well worked out.

-
Thanks a lot for your answer! What happens if $\hom(A,B)$ may be proper classes as well when $A$ and $B$ are arbitrary objects? Then, does $\exists!$ still make sense? This is probably a dumb question, but I don't really know what is or what is not allowed when the domain of quantification is not a set. Thanks!!! –  QcH May 5 '11 at 17:37
@Qph: I don't understand your comment: the collection of functions between any two sets is a set. –  Pete L. Clark May 5 '11 at 17:39
@Pete L. Clark: I was asking a general question related to big categories, and $\mathcal{Sets}$ is just an example demonstrating my question. –  QcH May 5 '11 at 17:52
@Qph: yes, you're right that such "big" (non-locally-small) categories sometimes arise, but this is not an issue. I think Emil has already answered you, but I'll say it in slightly different words: for any first-order formula $\phi$ with one free variable $x$, $\exists ! x \ \phi(x)$ is shorthand for the sentence $\exists x \ \phi(x) \wedge \forall x, y \ (\phi(x) \wedge \phi(y) \Rightarrow x = y$. –  Todd Trimble May 5 '11 at 18:00
Great! This clarifies a lot of things! Thanks a lot. –  QcH May 5 '11 at 18:03