Metamath Proof Explorer


Theorem fex2

Description: A function with bounded domain and range 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)

Ref Expression
Assertion fex2 F : A B A V B W F V

Proof

Step Hyp Ref Expression
1 xpexg A V B W A × B V
2 1 3adant1 F : A B A V B W A × B V
3 fssxp F : A B F A × B
4 3 3ad2ant1 F : A B A V B W F A × B
5 2 4 ssexd F : A B A V B W F V