von Neumann Universe as a model of ZFC

Question

I've seen people say things like "We will work in the von Neumann Universe (VNU) as our model of ZFC.” But can't you do all of mathematics syntatically, as in, come up with formal proofs in some proof system (e.g. natural deduction), since first-order logic is both sound and complete? And also, even if some formula is modeled by ZFC inside the VNU, it is not guaranteed for the same formula to hold in all models that model ZFC, so how is this first approach even legitimate?

Answer 1

The completeness theorem tells you that $ZFC \vdash \varphi$ if and only if $M \vDash \varphi$ for all models $M$ of ZFC. Hence, to prove a formula, just pick any model $M$ of ZFC. Since you accept regularity as part of ZFC, that means that $M$ is actually equal to the Von-Neumann Universe built inside $M$. That's why you can assume working in the VNU.