See Gödel's Incompleteness Theorems.
"Preliminary" formulation :
First incompleteness theorem : Any consistent formal system $F$ within which a "certain amount of elementary arithmetic" can be carried out is incomplete; i.e., there are statements of the language of $F$ which can neither be proved nor disproved in $F$.
Precise formulation :
Gödel's First Incompleteness Theorem : Assume $F$ is a formalized system which contains Robinson arithmetic $\mathsf Q$. Then a sentence $G_F$ of the language of $F$ can be mechanically constructed from $F$ such that:
If $F$ is consistent, then $F ⊬ G_F$.
If $F$ is $1$-consistent, then $F ⊬ ¬G_F$.
$\mathsf {ZFC}$ is precisely such a formalized system $F$ (i.e. "a formal system within which a 'certain amount of elementary arithmetic' can be carried out").
Gödel's original proof in his Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I ("On Formally Undecidable Propositions of Principia Mathematica and Related Systems I") does not use $\mathsf {ZFC}$ nor $\mathsf {PA}$.
His proof is relative to a "variant" of Principia Mathematica system; but his proof - in addition to esatblish the result now know as Gödel's Incompleteness Theorems - provides also a method applicable to many formal systems, provided that they satisfy some "initial conditions".
All the systems known as $\mathsf Q, \mathsf {PA}, \mathsf {ZFC}$ satisfy these conditions.
Relevant to your question, you can see :
It can be interesting to note that Melvin Fitting's thesis advisor was Raymond Smullyan.