Description: The set of injections between two classes exists if the codomain exists. (Contributed by AV, 14-Aug-2024)