This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fex2

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)

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 )