Description: Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017)