Metamath Proof Explorer


Theorem funexw

Description: Weak version of funex that holds without ax-rep . If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion funexw
|- ( ( Fun F /\ dom F e. B /\ ran F e. C ) -> F e. _V )

Proof

Step Hyp Ref Expression
1 xpexg
 |-  ( ( dom F e. B /\ ran F e. C ) -> ( dom F X. ran F ) e. _V )
2 1 3adant1
 |-  ( ( Fun F /\ dom F e. B /\ ran F e. C ) -> ( dom F X. ran F ) e. _V )
3 funrel
 |-  ( Fun F -> Rel F )
4 relssdmrn
 |-  ( Rel F -> F C_ ( dom F X. ran F ) )
5 3 4 syl
 |-  ( Fun F -> F C_ ( dom F X. ran F ) )
6 5 3ad2ant1
 |-  ( ( Fun F /\ dom F e. B /\ ran F e. C ) -> F C_ ( dom F X. ran F ) )
7 2 6 ssexd
 |-  ( ( Fun F /\ dom F e. B /\ ran F e. C ) -> F e. _V )