If something is provable in ZFC, can ZFC prove that ZFC proves it? IF ZFC proves a Well-formed formula, it means, 
if  $ZFC \vdash \phi$,
then, $ZFC \vdash (ZFC \vdash \phi$) ?
Generally, if an axiom system proves a wff, the axiom system can prove that it proves the fomula?
 A: Yes, but not conversely.
If $T$ is a recursive theory that is strong enough to internalise FOL via the standard methods,1 then all "real" statements in the language of $T$ get coded via standard codes, and all proofs are of finite length which lets us code real proofs in a way that is compatible with the internalisation of FOL.
You can prove this easily by induction on the complexity of the formula, that a standard formula gets assigned a standard code, and then by the definition of the provability predicate.
If $T$ is not recursive, you will need an oracle for it anyway, but the above arguments apply.
Note that in the other direction of the implication, if $T$ is consistent but actually proves $\lnot\operatorname{Con}(T)$, then $T$ does not prove $0=1$, but it proves that it proves $0=1$ (because the internal proof is not standard anymore).



*

*Note that in PA this means Gödel codes, but in ZFC we can actually code things via finite strings as objects in $V_\omega$ instead. This makes more intuitive sense, and if you know that $V_\omega$ is "essentially $\omega$", then you can move between Gödel codes and actual finite sequences freely enough.

