One schema for all sets
I was thinking of coining a single comprehension axiom schema in the language of set theory that can interpret all axioms of ZFC, provided the scheme is *not a trivial conjunction of all axioms of ZFC*. Here is a try:
**Comprehension:** if $\phi(x,y,A_1,A_2)$ is a formula in which all and only symbols $``x,y,A_1,A_2"$ occur free, and only free, then:
$$\forall A_1,A_2 [\forall x \ \exists z \ \forall y \ (\phi(x,y,A_1,A_2) \to y \leq^h z) \to \exists B \forall y (y \in B \leftrightarrow \exists x \underline{\in} A_2 [\phi(x,y,A_1,A_2)])]$$, is an axiom.
Where $\underline{\in}$ denotes "is a member of or is equal to", defined as: $x \underline{\in} y \iff x \in y \lor x=y$
where $``\leq^h"$ stands for "is hereditarily subnumerous to" defined as:
$$ y \leq^h z \iff y \leq z \wedge \exists c [\forall x \in c(x \subset c \wedge x \leq z) \wedge y \subseteq c]$$, and $``\leq"$ is defined as: $$ y \leq z \iff y \subseteq z \ \lor \exists f (f: y \to z \ \wedge f \text{ is an injection})$$
where an "injection" is defined in the standard manner.
This scheme is a kind of a replacement schema whereby for each set $A$ we can replace each element $m$ of $A$ (or replace $A$ itself) by sets as long as all of those sets are hereditarily subnumerous to a common set (per each $m$).
Now I think this would interpret [Union+Power+Separation+Collection+Infinity] over the realm of "subsets of transitive sets", and this is known to interpret ZFC. Now the above scheme is a theorem schema of ZFC. So the above single scheme has the same consistency strength as ZFC. I've been surfing the web for short interpretations of set theory, to find few examples that are not as short. However that matter must have been investigated before?
>**Question:** what are the known short interpretations of ZFC? i.e. a fragment of ZFC that is a single schema that can interpret all of ZFC? I'm looking for ones reducing ZFC to be interpreted in a SINGLE schema in the language of set theory itself, i.e. in the first order language of membership and identity? provided that the schema is not a trivial re-formulation of ZFC?