Description: If a function value has a member, then the function is not an empty set (An artifact of our function value definition.) (Contributed by Zhi Wang, 16-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elfvne0 | |- ( A e. ( F ` B ) -> F =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ne0i | |- ( A e. ( F ` B ) -> ( F ` B ) =/= (/) ) |
|
| 2 | fveq1 | |- ( F = (/) -> ( F ` B ) = ( (/) ` B ) ) |
|
| 3 | 0fv | |- ( (/) ` B ) = (/) |
|
| 4 | 2 3 | eqtrdi | |- ( F = (/) -> ( F ` B ) = (/) ) |
| 5 | 4 | necon3i | |- ( ( F ` B ) =/= (/) -> F =/= (/) ) |
| 6 | 1 5 | syl | |- ( A e. ( F ` B ) -> F =/= (/) ) |