Description: The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | elrnmptd.f | |- F = ( x e. A |-> B ) |
|
elrnmptd.x | |- ( ph -> E. x e. A C = B ) |
||
elrnmptd.c | |- ( ph -> C e. V ) |
||
Assertion | elrnmptd | |- ( ph -> C e. ran F ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrnmptd.f | |- F = ( x e. A |-> B ) |
|
2 | elrnmptd.x | |- ( ph -> E. x e. A C = B ) |
|
3 | elrnmptd.c | |- ( ph -> C e. V ) |
|
4 | 1 | elrnmpt | |- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) ) |
5 | 3 4 | syl | |- ( ph -> ( C e. ran F <-> E. x e. A C = B ) ) |
6 | 2 5 | mpbird | |- ( ph -> C e. ran F ) |