Theorem afv0fv0

Description: If the value of the alternative function at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	afv0fv0	|- ( ( F ''' A ) = (/) -> ( F ` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		eleq1a	|- ( (/) e. _V -> ( ( F ''' A ) = (/) -> ( F ''' A ) e. _V ) )
3	1 2	ax-mp	|- ( ( F ''' A ) = (/) -> ( F ''' A ) e. _V )
4		afvvfveq	|- ( ( F ''' A ) e. _V -> ( F ''' A ) = ( F ` A ) )
5		eqeq1	|- ( ( F ''' A ) = ( F ` A ) -> ( ( F ''' A ) = (/) <-> ( F ` A ) = (/) ) )
6	5	biimpd	|- ( ( F ''' A ) = ( F ` A ) -> ( ( F ''' A ) = (/) -> ( F ` A ) = (/) ) )
7	4 6	syl	|- ( ( F ''' A ) e. _V -> ( ( F ''' A ) = (/) -> ( F ` A ) = (/) ) )
8	3 7	mpcom	|- ( ( F ''' A ) = (/) -> ( F ` A ) = (/) )