Description: The domain of a one-to-one function is dominated by its codomain. This variation of f1domg does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015)