As cody pointed out to me, this answers the question from the viewpoint of a mathematical platonist.
There are 2 different ZFCs. First is the ZFC that we work in, the one we know and love. In this ZFC, a "proof" means what we mean colloquially by a "proof". In this "casual": ZFC, helped by our real world intuition and experience, we know that "A and B" means what it does in english: both A and B are true. We know what "A(x) is true for all x" means - what it does in english. We know that 2+2=4, not because of number theory or the Peano axioms, but because that reflects our daily experience. We learn how to recognize proofs, not by their ability to be transformed into formal language, but by experience, intuition, and gut feeling.
Within this "casual" ZFC, we create the rigorous discipline known as logic. Within this logic, we formalize the notion of "truth", we formalize the notion of "proof", we formalize, well, everything. Most of our definitions which formalize these notions are based on our feelings/experience in "casual" ZFC. For example, in logic, we define $(A\wedge B)$ to hold if and only if $A$ holds and $B$ holds.
Finally, within logic, we define "formal" ZFC. Here, ZFC is a list of axioms and "proof" means "a chain of sentences, each of which is either a hypothesis, axiom, or can be formally deduced from a previous sentence in the chain by modus ponens." "Truth" becomes a semantic notion, often depending on which particular model of ZFC we are working with.