Working in first order logic with equality and membership, add the following axiom schemata:
- Specification:$(\exists! i:i=\{x \in A \mid \phi\})$; if $``i"$ not used by $\phi$.
- Reflection:$(\phi \to \exists \alpha: \phi^{V_\alpha} \land |V_\alpha|=\alpha)$; if $``\alpha"$ not used by $\phi$.
Where: $V_\alpha$ and $||$ are defined in the customary manner; and $\phi^{V_\alpha}$ is the bounded by $V_\alpha$ form of formula $\phi$.
This system proves all axioms of ZFC.
I know that ZFC proves $(\phi \to \exists \alpha: \phi^{V_\alpha})$, also it proves that every set belongs to some stage $V_\alpha$ where $|V_\alpha|=\alpha$. But, does it prove the Reflection axiom stated above? Or can this axiom be actually inconsistent with ZFC?