Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rnmptssd.1 | |- F/ x ph |
|
rnmptssd.2 | |- F = ( x e. A |-> B ) |
||
rnmptssd.3 | |- ( ( ph /\ x e. A ) -> B e. C ) |
||
Assertion | rnmptssd | |- ( ph -> ran F C_ C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnmptssd.1 | |- F/ x ph |
|
2 | rnmptssd.2 | |- F = ( x e. A |-> B ) |
|
3 | rnmptssd.3 | |- ( ( ph /\ x e. A ) -> B e. C ) |
|
4 | 1 3 | ralrimia | |- ( ph -> A. x e. A B e. C ) |
5 | 2 | rnmptss | |- ( A. x e. A B e. C -> ran F C_ C ) |
6 | 4 5 | syl | |- ( ph -> ran F C_ C ) |