Description: A function with bounded domain and codomain is a set. This version of
fex is proven without the Axiom of Replacement ax-rep , but depends on
ax-un , which is not required for the proof of fex . (Contributed by Mario Carneiro, 24-Jun-2015)