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 ) |
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 ) |