Description: If a set is in the range of a function, the function's value at an argument is the empty set if and only if the alternate function value at this argument is either the empty set or undefined. (Contributed by AV, 11-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | afv2fv0xorb | |- ( (/) e. ran F -> ( ( F ` A ) = (/) <-> ( ( F '''' A ) = (/) \/_ ( F '''' A ) e/ ran F ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | afv2fv0b | |- ( ( F ` A ) = (/) <-> ( ( F '''' A ) = (/) \/ ( F '''' A ) e/ ran F ) ) |
|
| 2 | afv2orxorb | |- ( (/) e. ran F -> ( ( ( F '''' A ) = (/) \/ ( F '''' A ) e/ ran F ) <-> ( ( F '''' A ) = (/) \/_ ( F '''' A ) e/ ran F ) ) ) |
|
| 3 | 1 2 | syl5bb | |- ( (/) e. ran F -> ( ( F ` A ) = (/) <-> ( ( F '''' A ) = (/) \/_ ( F '''' A ) e/ ran F ) ) ) |