Garabed, I believe the class of surreals can be encoded by a class formula in ZFC.

Surreal numbers are particular kinds of Conway games, and each Conway game can be expressed as a well-founded rooted tree of bounded (i.e., non-class) size equipped with a labeling of the edges by symbols $L$ and $R$. (The nodes are positions in the game, with the root at initial position, and an edge from a node to a child is labeled $L$ or $R$ according to whether the child is a left or right option of the node.) So the full structure of a Conway game is fully specified by a set, and the notion of Conway game can be given by a ZFC formula. The relation $\lt$ on games, and the predicate that says a game is a number, are recursive and can be given by formulas in ZFC. Similarly, the equality predicate on numbers is recursive and given by a ZFC formula.

I don't have On Numbers and Games immediately to hand, but my memory is that Conway discusses these issues.

Garabed, I believe the class of surreals can be encoded by a class formula in ZFC.

Surreal numbers are particular kinds of Conway games, and each Conway game can be expressed as a well-founded rooted tree of bounded (i.e., non-class) size equipped with a labeling of the edges by symbols $L$ and $R$. (The nodes are positions in the game, with the root at initial position, and an edge from a node to a child is labeled $L$ or $R$ according to whether the child is a left or right option of the node.) So the full structure of a Conway game is fully specified by a set, and the class of Conway games can be given by a ZFC class formula. The relation $\lt$ on games, and the predicate that says a game is a number, are recursive and can be given by formulas in ZFC. Similarly, the equality predicate on numbers is recursive and given by a ZFC formula.

I don't have On Numbers and Games immediately to hand, but my memory is that Conway discusses these issues.