There is a fragment of ZFC once introduced by Hjorth, it contains first one million of ZFC axioms (which must include all single axioms) plus Replacement (or Collection) for all Sigma_100 formulas. I believe this is enough to prove any known at the moment particular theorem of ZFC. V.Kanovei