Theorem afv2fv0

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

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

Proof

Step	Hyp	Ref	Expression
1		ioran	|- ( -. ( ( F '''' A ) = (/) \/ ( F '''' A ) e/ ran F ) <-> ( -. ( F '''' A ) = (/) /\ -. ( F '''' A ) e/ ran F ) )
2		nnel	|- ( -. ( F '''' A ) e/ ran F <-> ( F '''' A ) e. ran F )
3		afv2rnfveq	|- ( ( F '''' A ) e. ran F -> ( F '''' A ) = ( F ` A ) )
4	2 3	sylbi	|- ( -. ( F '''' A ) e/ ran F -> ( F '''' A ) = ( F ` A ) )
5	4	eqeq1d	|- ( -. ( F '''' A ) e/ ran F -> ( ( F '''' A ) = (/) <-> ( F ` A ) = (/) ) )
6	5	notbid	|- ( -. ( F '''' A ) e/ ran F -> ( -. ( F '''' A ) = (/) <-> -. ( F ` A ) = (/) ) )
7	6	biimpac	|- ( ( -. ( F '''' A ) = (/) /\ -. ( F '''' A ) e/ ran F ) -> -. ( F ` A ) = (/) )
8	1 7	sylbi	|- ( -. ( ( F '''' A ) = (/) \/ ( F '''' A ) e/ ran F ) -> -. ( F ` A ) = (/) )
9	8	con4i	|- ( ( F ` A ) = (/) -> ( ( F '''' A ) = (/) \/ ( F '''' A ) e/ ran F ) )