The following is taken from Borceux and Bourn's Mal'cev, Protomodular, Homological, and Semi-Abelian Categories.
Metatheorem 0.1.3. Let $\mathcal P$ be a statement of the form $\varphi\implies \psi$, where $\varphi$ and $\psi$ can be expressed as conjunctions of properties in the following list:
- some finite diagram is commutative;
- some morphism is a monomorphism;
- some morphism is an isomorphism;
- some finite diagram is a limit diagram;
- an arrow $f:\rightarrow B$ factors (of course, uniquely) through some specified monomorphism $s:S\rightarrowtail B$.
If this statement is valid in the category of sets, it is valid in every category.
After the proof comes the following remark.
It is probably useful to make a comment. The list of properties in our metatheorem is not exhaustive. A better way to express the metatheorem would have been to state it for Horn sentences and the "unique existential quantifier $\exists!$", but we do not want to enter those considerations here.
I tried googling 'Yoneda embedding horn sentence' but didn't find anything I thought was relevant. What is the "better way to express the metatheorem", and why is it true? I'm guessing some topos theory comes in, but I don't really know anything about (the logical aspect of) it.