Theorem afv2fv0b

Description: The function's value at an argument is the empty set if and only if the alternate function value at this argument is the empty set or undefined. (Contributed by AV, 3-Sep-2022)

	Ref	Expression
Assertion	afv2fv0b	|- ( ( F ` A ) = (/) <-> ( ( F '''' A ) = (/) \/ ( F '''' A ) e/ ran F ) )

Proof

Step	Hyp	Ref	Expression
1		afv2fv0	|- ( ( F ` A ) = (/) -> ( ( F '''' A ) = (/) \/ ( F '''' A ) e/ ran F ) )
2		afv20fv0	|- ( ( F '''' A ) = (/) -> ( F ` A ) = (/) )
3		afv2ndeffv0	|- ( ( F '''' A ) e/ ran F -> ( F ` A ) = (/) )
4	2 3	jaoi	|- ( ( ( F '''' A ) = (/) \/ ( F '''' A ) e/ ran F ) -> ( F ` A ) = (/) )
5	1 4	impbii	|- ( ( F ` A ) = (/) <-> ( ( F '''' A ) = (/) \/ ( F '''' A ) e/ ran F ) )