This post is a follow up of this one posted to MathStackExchange.
Working in $\sf ZFC + \exists M \, (M \overset{trs} \models ZFC)$, lets define a theory $T_0$ as:
$$(\varphi \ \epsilon \ T_0) \iff \forall M ((M \overset {\sf min \ trs} \models {\sf ZFC}) \implies (M \models \varphi))$$
Where $\sf trs$ stands for 'transitive', and $\sf min$ for 'minimal'. The symbol "$\epsilon$" is a metatheortic relation symbol standing for membership of sentences in theories, $T_0$ is a metatheoretic constant symbol standing for some specific set of sentences. Of course $\varphi$ is a metatheoretic variable ranging over all sentences of the first order language of set theory.
$T_0$ is recursively enumerable, but what could be the axioms of it, other than the trivial case of making every $\varphi$ sentence satisfying the right hand being an axiom of $T_0$.
I mean is there another way of defining the metatheoretic predicate $\text { is an axiom of } T_0$ after inability of an element of $T_0$ to be deduced in $T_0$ from other elements? That is, the basis for it being an axiom is that it requires a proof in the mother theory of it fulfilling the right hand of the characterization of $T_0$, i.e. the proof of its enrollment in $T_0$ must be external to provability in $T_0$.
How can one do that formally?
If that can be done, what are the axioms explicity, would it be for example? $$\sf ZFC + V=L + \neg \exists M \, (M \overset {trs} \models ZFC)$$
