This question is primarily a reference request. It arose from a personal coding/formalization project.

I am using a particular form of a definition of a category in ZFC. According to this definition, the sets $V_{\alpha}$ for limit ordinals $\alpha$ such that $\omega < \alpha$ replace the Groethendick universes in the more conventional setting for the definition of a category. This approach is similar to what was originally proposed in Set-Theoretical Foundations of Category Theory and later promoted in Set Theory for Category Theory and a few other expository articles.

The primary problem associated with this definition is related to the lack of the Axiom of Replacement "closed in $V_{\alpha}$". However, various tricks were developed in the aforementioned articles to avoid this problem. Unfortunately, some of the theory behind these tricks seemed to be quite challenging to formalize using the technology that I was using (not impossible, but quite unwieldy and labor-intensive).

I have done some experiments in an attempt to avoid some of the aforementioned difficulties, and I found that the following condition is quite natural for the definition of a locally-small category in this setting (and I hardly need anything larger than locally small for what I am doing): \begin{equation} \forall A \subseteq \mathcal{C}_{Obj}. \forall B \subseteq \mathcal{C}_{Obj}. A \in V_{\alpha} \longrightarrow B \in V_{\alpha} \longrightarrow \bigcup_{a \in A} \bigcup_{b \in B} \text{Hom}_{\mathcal{C}} (a, b) \in V_{\alpha} \end{equation} In this case, $\mathcal{C}_{Obj}$ can still be any subset of $V_{\alpha}$. This condition also implies that the Hom-sets are small. However, this condition still has to be combined with some of the simpler tricks described in Set Theory for Category Theory (e.g., to quote, "the correct definition of complete is 'having limits for all small functors'"), and I had to come with a few further tricks of my own to make the theory work. One important aspect of this condition (what I believe makes it work well) is that it provides closure with respect to taking the functor categories. That is, $\mathcal{C}^{\mathcal{J}}$ is locally small provided that $\mathcal{C}$ is locally small and $\mathcal{J}$ is small.

My access to research literature is very limited at the moment and I have little social connection with the fields of foundations/pure mathematics. Therefore, I am not certain whether the aforementioned definition is already available in the research literature somewhere or, perhaps, it is part of the "folklore" already. Thus, my primary question is whether anyone had seen the aforementioned condition before in the context of a definition of a locally-small category in ZFC.

The secondary question is whether anyone can suggest any important theorem that holds in the conventional setting with the reference to locally small 1-categories but will fail when using the proposed condition. Thus far, I was able to find a way around such problems by strengthening the conditions for a given theorem to hold slightly (e.g., I coded Yoneda and the Freyd General Adjoint Theorem).

P.S. I tried asking a similar question on MSE some time ago, but received very few comments.