@bof: You could always ignore my.. err.. son...

I think it's impossible to reach ZFC strength by any means that can be considered predicative. At the best, ZFC with only bounded Specification and Replacement. The reason is that Replacement makes absolutely no sense unless you already believe in something as strong as ZFC.

Does it satisfy "ZFC is arithmetically sound"?

@AlexisHazell: And there is no finite axiomatization of ZFC. Nevertheless, ZFC has a finitely axiomatizable conservative extension. Generally, any formal system based on FOL can be converted into a finitely axiomatizable FOL theory with the same strength, so infiniteness of axioms is not an intrinsic characteristic of a formal system.

Besides the post on circularity that Asaf linked to, see also this post on building blocks. Essentially, when you want to set up FOL for actual concrete formal systems, and reason about it, you need only ACA, which supports reasoning about ℕ and subsets of ℕ that have an arithmetical defining formula. You do not need actually set-theoretic assumptions.

This does not support ZFC with Replacement. Boolos said so explicitly himself; he said that Replacement is "not derived from the iterative conception". Moreover, almost all modern mathematics can be done within B[ounded]ZFC (i.e. with both Specification and Replacement restricted to Δ0 defining formulae), and this is at least reasonably cogent and in line with the iterative conception, in contrast to the unjustified unbounded schemas. We can conceivably extend to BZFC^P, where "^P" means that powerset is an inbuilt function-symbol, and BZFC^P suffices for essentially all ordinary mathematics.

@EmilJeřábek: 2 = (1+1). 3 = (1+1)+1. 4 = ((1+1)+1)+1. I made a mistake with the 5th axiom, sorry..

Of course you can stop and leave at any point, especially if you cannot refute my points, even though they are simple and pertinent. It is completely well-known to experts that the proper strength scale for fragments of ZFC is the one given by Σ[n]-Rep[lacement], very like the proper strength scale for fragments of PA is the one given by Σ[n]-Ind[uction]. Your misconception about the strength of Powerset is because you're not looking at anything near the full strength of ZFC. Σ[n]-Rep is the n-th rung of the real ladder, while Powerset is on the floor below the 1st rung.

To give you a concrete example, look at this theory, which has no Powerset but obviously has impredicative reflection.

@FedorPakhomov: You didn't refute a statement I didn't intend to make. I didn't mean it didn't contribute anything; I intended to say that impredicativity is critical to the strength of ZFC, not Powerset. Consider that ZFC without the underlying (classical) FOL rules cannot do anything, whereas ZFC−Powerset is as strong as SOA. You cannot by this infer that FOL contributes immense strength to ZFC compared to Powerset! To say in another way: Every system that can reach the strength of ZFC must have some impredicative reflection (e.g. unbounded Replacement).