The following is a reformulation of $\sf ZFC$, it is a version of a well known approach going back to Dana Scott (I suppose), it axiomatizes $\sf ZFC$ simply by "Specification, Reflection, and Choice".
The language of this theory is first order logic with equality and membership, and as usual definitions are allowed to be added to the background logic, so we have as many defined predicate and function symbols as their defining formulas.
Axioms:
Specification: if $\phi$ is a tri-parameteric formula, not using "$Y$", then: $$.. \forall X \, \exists! Y \, \forall z \, (z \in Y \iff z \in X \land \phi)$$
Reflection: if $\varphi$ is a mono-parameteric formula, not using "$\alpha$", and $\varphi^{V_\alpha}$ is the "$\in V_\alpha$" bounded form of $\varphi$, then: $$ ( \varphi \implies \exists \alpha: \varphi^{V_\alpha})$$
Choice: as in $\sf ZFC$.
$V_\alpha$ is defined in the customary manner as: the image of ordinal $\alpha$ under a function from an ordinal that assigns to each element the set of all subsets of images it assigns to prior elements; ordinal is defined as being a set of all transitive proper subsets of it.
Note that there is no restrection on using defined predicate and function symbols in above schemata.
This reformulation is highly technical and by no means naive. But, I'd prefer it when contemplating extending $\sf ZFC$ with large cardinal axioms since reflection is at the heart of such extensions.
Are there known simpler reformulations of $\sf ZFC$ that more suits that purupose? like using embeddings instead of reflection, or perhaps some other way altogether?
