Theorem afv20fv0

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

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

Proof

Step	Hyp	Ref	Expression
1		afv20defat	|- ( ( F '''' A ) = (/) -> F defAt A )
2		dfatafv2eqfv	|- ( F defAt A -> ( F '''' A ) = ( F ` A ) )
3	2	eqcomd	|- ( F defAt A -> ( F ` A ) = ( F '''' A ) )
4	3	adantr	|- ( ( F defAt A /\ ( F '''' A ) = (/) ) -> ( F ` A ) = ( F '''' A ) )
5		simpr	|- ( ( F defAt A /\ ( F '''' A ) = (/) ) -> ( F '''' A ) = (/) )
6	4 5	eqtrd	|- ( ( F defAt A /\ ( F '''' A ) = (/) ) -> ( F ` A ) = (/) )
7	1 6	mpancom	|- ( ( F '''' A ) = (/) -> ( F ` A ) = (/) )