It depends what you mean by "work."
If you just want to show that a program never exhibits some simple behavior - e.g., if you want to show it doesn't halt - then if ZFC proves this fact, it's correct, as long as ZFC is consistent.
If you want to show that a program will at some point exhibit some simple behavior - e.g., if you want to show it will halt - then knowing the correctness of a ZFC-proof requires a bit more than just the assumption that ZFC is consistent - we need to know that it is $\Sigma^0_1$-sound. This is a technical hypothesis much weaker than the assumption "Every arithmetical consequence of ZFC is true" (which we usually assume).
And, of course, Gödel's theorem shows that ZFC won't always be enough, even for the simplest statements - there is a Turing machine $T$ which never halts (assuming ZFC is consistent) but which ZFC can't prove never halts (again, assuming ZFC is consistent).
But these are general problems you'll have with any background theory, not just ZFC. Every result of this type - actually, every result at all - exists in the context of background assumptions. ZFC happens to occupy that sweet spot of (a) being extremely common to assume, (b) reasonably well-understood, and (c) powerful enough to handle almost all "reasonable" problems. (One can try to make stronger arguments for ZFC as opposed to other theories, but that's a problem for another time.) So the answer to why we use ZFC: well, we gotta use something. :)
This is because the framework described by the NBG axioms is strictly richer than that which the ZFC axioms describe. This is not an isolated phenomenon. Let me show you diffrent, perhaps a bit less abstract examples.
First example.
It is a well-known consequence of compactness that there is no first-order axiom in the language with just equality whose models are exactly the infinite sets. We need infinitely many axioms saying that there are at least $n$ elements, for arbitrarily large $n$.
On the other hand, if we add a linear ordering, we can consider the theory of dense linear orderings (with at least two points), which is finitely axiomatisable and has no finite models.
Every infinite set can be expanded to a dense linear ordering. Thus, the pure sets underlying dense linear orderings are exactly all infinite sets.
Second example.
For a field $F=(F,+,\cdot,0,1)$, the following are equivalent:
- $F$ is formally real, i.e. whenever a sum of squares is zero, all of them have to be zero.
- There is a linear ordering $\leq$ on $F$ which is compatible with the field operations (making $(F,+,\cdot,0,1,\leq)$ an ordered field).
Now, the first order of formally real fields is not finitely axiomatisable: for any $n$, there is a field which is not formally real, but such that the sum of at most $n$ squares, not all zero, is necessarily nonzero. The conclusion follows by compactness.
On the other hand, the theory of ordered fields is obviously finitely axiomatisable.
In this case, the pure fields described by the (finitely axiomatisable) theory of ordered fields are exactly the same as the pure fields described by the (not finitely axiomatisable) theory of formally real fields.
In both examples, the extra structure provided by the linear ordering allows us to force infinitely many axioms to hold simultaneously. Similarly, for NBG, the extra structure provided by the addition of proper classes as elements allows us to force infinitely many axioms to hold simultaneously.
In all cases, the cost is that we need to choose this extra structure: there are many ways to choose a dense linear ordering of an infinite sets, there are (typically) many ways to choose a compatible linear ordering for a formally real field, and there are also (typically?) many ways to expand a model of ZFC to a model of NBG - a pure set does not know its dense linear orderings, a formally real field (usually) does not know any particular compatible ordering, and there is no reason for a model of ZFC to know what classes you should endow it with to get a model of NBG.
Best Answer
In the comments, you clarified your question:
Well, you can open up literally any introductory logic textbook. An example of such a system (which is called a natural deduction system) is described on wikipedia here.
In my answer here, I wrote out all the details of a natural deduction proof that the empty set is unique.