### Using a reflection principle for ZFC

Zermelo-Fraenkel set theory with choice, ZFC, is a first-order theory with an infinite number of axioms. For every finite subset A1,A2,..An of axioms of ZFC, the following is provable in ZFC:
(1) There is a model of the axioms A1,A2,..An, i.e. an interpretation that makes them all true.
Since a theory with a model is necessarily consistent, this means that the following is also provable in ZFC for every such finite subset A1,A2,..An:
(2) The theory with axioms A1,A2,..An is consistent.
We can also prove in ZFC the trivial fact that
(3) If ZFC is inconsistent, then the theory with axioms A1,A2,..An is inconsistent, for some finite subset A1,A2,..An of axioms of ZFC.
We can thus conclude, using the axioms of ZFC, that the axioms of ZFC are consistent: by (2) every finite set of axioms of ZFC is consistent (provably in ZFC), so by (3) ZFC is consistent.

Why can't this proof be carried out in ZFC? The answer lies in the difference between

For every finite set A1,A2,..An of axioms of ZFC, it is provable in ZFC that these axioms are consistent
and
It is provable in ZFC that for every finite set A1,A2,..An of axioms of ZFC, these axioms are consistent
Only the first of these statements is true, not the second. When we conclude from
For every finite set of axioms A1,A2,..An of ZFC, it is provable in ZFC that A1,A2,..An form a consistent set
to
Every finite set A1,A2,..An of axioms of ZFC is a consistent set
we are using a principle not provable in ZFC: the principle that whenever a statement of the form "the formulas A1,A2,..An have property P" is provable in ZFC for all formulas A1,A2,..An, then all formulas A1,A2,..An do have the property P. This is a so-called reflection principle for ZFC, and is not provable in ZFC itself (by Gödel's second theorem).