Description: A function value is a subset of the union of the range. (An artifact of our function value definition, compare elfvdm ). (Contributed by Thierry Arnoux, 13-Nov-2016) Remove functionhood antecedent. (Revised by SN, 10-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elfvunirn | |- ( B e. ( F ` A ) -> B e. U. ran F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ne0i | |- ( B e. ( F ` A ) -> ( F ` A ) =/= (/) ) |
|
| 2 | fvn0fvelrn | |- ( ( F ` A ) =/= (/) -> ( F ` A ) e. ran F ) |
|
| 3 | elssuni | |- ( ( F ` A ) e. ran F -> ( F ` A ) C_ U. ran F ) |
|
| 4 | 1 2 3 | 3syl | |- ( B e. ( F ` A ) -> ( F ` A ) C_ U. ran F ) |
| 5 | 4 | sseld | |- ( B e. ( F ` A ) -> ( B e. ( F ` A ) -> B e. U. ran F ) ) |
| 6 | 5 | pm2.43i | |- ( B e. ( F ` A ) -> B e. U. ran F ) |