lo.logic – Can this reflexive class theory interpret ZFC?

Theory of reflective sets $ mathsf {RfST} $ is formulated in a first-order predicate logic with extra-logical equality primitives $ “ = "$membership $ “ in "$, and a single constant primitive symbol $ V $ designating the class of all sets.

Axioms are those of the theory of the first order identity +

  1. extensionality: $ forall x (x in a leftrightarrow x in b) to a = b $

  2. Class comprehension: if $ varphi (y) $ is a formula in which the symbol $ “ y "$ occurs free, so all closures of: $ exists x forall y (y in x leftrightarrow y in V wedge varphi (y)) $ are axioms.

  3. Reflection: if $ varphi (y, x_1, .., x_n) $ is a formula in $ FOL (=, in) $, in which only $ y, x_1, .., x_n $ occur for free, then:

$$ forall x_1, .., x_n in V \ [exists y (varphi(y,x_1,..,x_n)) to exists y in V (varphi(y,x_1,..,x_n))]$$

is an axiom

  1. Transitive: $ forall x in V forall y in x (y in V) $

  2. Foundation: $ exists m in x to exists y in x forall z in x (z not in y) $

/ Definition of the completed theory.

Personally, I think this axiometry is the most elegant theory of sets / classes I know!

Can this theory interpret $ ZFC $ more than $ L $?

I speak clearly of the axioms of matching, union, separation and replacement $ V $ pure formulas, the infinite, are all provable here, but the power is not easily provable here, but all together $ V $ it's an element of a scene $ L _ { kappa} $, would have all his subsets in $ L _ { kappa} $ to be in $ V $because they are all definable by well-defined formulas; we must therefore be able to reflect the existence of a set of all these subsets inside. $ V $, thus interpreting $ ZFC + V = L $.