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