Fitch-style set theory proofs

Question

Suppose I'm working in ZFC and I'm trying to prove that the empty set is a subset of any set. How would one formalize that in FOL style? To be more clear, in FOL, proofs are of the form $\Gamma\vdash \varphi$, where $\Gamma$ is some set of wffs and $\varphi$ is a wff. My question is where would the ZFC axioms fit in that? Would they be included in $\Gamma$, would they get incorporated into the proof system alongside the logical axioms? Would it be written as \begin{align*} \vdash \forall x\forall w (w\in \emptyset \to w\in x) \end{align*} or as \begin{align*} \text{ZFC}\vdash \forall x\forall w (w\in \emptyset \to w\in x) \end{align*} where ZFC is the set of ZFC axioms in the Theory of ZFC? Am I making any sense? And while I'm at it, are there any books that carry out those proofs in, say Fitch-style natural deduction?