Description: If the codomain of a function is a set, the alternate function value is always also a set. (Contributed by AV, 4-Sep-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | frnvafv2v | |- ( ( F : A --> B /\ B e. V ) -> ( F '''' C ) e. _V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f | |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) ) |
|
2 | ssexg | |- ( ( ran F C_ B /\ B e. V ) -> ran F e. _V ) |
|
3 | 2 | ex | |- ( ran F C_ B -> ( B e. V -> ran F e. _V ) ) |
4 | 1 3 | simplbiim | |- ( F : A --> B -> ( B e. V -> ran F e. _V ) ) |
5 | 4 | imp | |- ( ( F : A --> B /\ B e. V ) -> ran F e. _V ) |
6 | afv2ex | |- ( ran F e. _V -> ( F '''' C ) e. _V ) |
|
7 | 5 6 | syl | |- ( ( F : A --> B /\ B e. V ) -> ( F '''' C ) e. _V ) |