Theorem fex2

Description: A function with bounded domain and range is a set. This version of fex is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Assertion	fex2	|- ( ( F : A --> B /\ A e. V /\ B e. W ) -> F e. _V )

Proof

Step	Hyp	Ref	Expression
1		xpexg	|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
2	1	3adant1	|- ( ( F : A --> B /\ A e. V /\ B e. W ) -> ( A X. B ) e. _V )
3		fssxp	|- ( F : A --> B -> F C_ ( A X. B ) )
4	3	3ad2ant1	|- ( ( F : A --> B /\ A e. V /\ B e. W ) -> F C_ ( A X. B ) )
5	2 4	ssexd	|- ( ( F : A --> B /\ A e. V /\ B e. W ) -> F e. _V )