Metamath Proof Explorer


Theorem afv2fv0xorb

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 ) ) )

Proof

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 ) ) )