How many proofs in the language of ZFC are there? I would say countably infinite, since every proof is a finite sequence of symbols over a finite alphabet (e.g. ASCII).
Consider the proof in https://proofwiki.org/wiki/Woset_is_Isomorphic_to_Unique_Ordinal. In its essence, the reasoning is as follows:
Let $(W, \prec)$ be a well-ordered set. From $(W, \prec)$ construct a well-order of well-orders $(W', \prec')$ which contains $(W, \prec)$ as its largest element. Prove by transfinite induction over $(W', \prec')$ that any of its elements is order-isomorphic to some ordinal. Since $(W, \prec)$ is an element of $(W', \prec')$, $(W, \prec)$ is order-isomorphic to an ordinal. As $(W, \prec)$ was arbitrary, conclude that every well-ordered set is order-isomorphic to an ordinal.
Sounds reasonable. But isn't this exactly the same as saying:
For all well-ordered sets there exists a proof* (by transfinite induction), that proves the existence of an ordinal that is order-isomorphic to that set.
So have we just instantiated proper-class-many ZFC-proofs? Moreover, the existential quantifier quantifies over a proof, not a set, so the reasoning is a meta-proof at most? I don't want proof* to be interpreted as a set that encodes a ZFC-proof inside models of ZFC, because in that models there could exist proofs* of non-standard-integer lengths, correct?
Is this meta-proof valid?
EDIT:
The $\forall x: x=x$ example actually helped, but in a different way.
My thinking was, that a proof of the form "Let $x$ with $P(x)$ be arbitrary, then infer $\phi(x)$" is a prosaic inference of the formula $\forall x: P(x) \rightarrow \phi(x)$ by using inference rules from quantified formulae to quantified formulae. Furthermore have I thought that a hilbert system includes $\forall x: x=x$ implicitly as an axiom. So for your counterexample, there was no need to talk about proofs of $x=x$ for every $x$. For the well-order case however, I could not imagine how the deduction would look like. The reasoning why transfinite induction works on a specific well-ordered set is shown by contradiction. But how could I "suppose otherwise" inside the formula $\forall W ( ... )$? So my conclusion was, that the proof indended to show the existence of proofs.
That said, I see now what I have missed. A hilbert system factually includes $x=x$ for every variable $x$, and via universal generalization one can infer $\forall x: x=x$. Similarly, the well-order proof actually proves a formula that is free in $W$, and the generalization is then implicit.
Sorry and thank you.