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	⊢ ( ( 𝐹 '''' 𝐴 ) = ∅ → ( 𝐹 ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		afv20defat	⊢ ( ( 𝐹 '''' 𝐴 ) = ∅ → 𝐹 defAt 𝐴 )
2		dfatafv2eqfv	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
3	2	eqcomd	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 '''' 𝐴 ) )
4	3	adantr	⊢ ( ( 𝐹 defAt 𝐴 ∧ ( 𝐹 '''' 𝐴 ) = ∅ ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 '''' 𝐴 ) )
5		simpr	⊢ ( ( 𝐹 defAt 𝐴 ∧ ( 𝐹 '''' 𝐴 ) = ∅ ) → ( 𝐹 '''' 𝐴 ) = ∅ )
6	4 5	eqtrd	⊢ ( ( 𝐹 defAt 𝐴 ∧ ( 𝐹 '''' 𝐴 ) = ∅ ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
7	1 6	mpancom	⊢ ( ( 𝐹 '''' 𝐴 ) = ∅ → ( 𝐹 ‘ 𝐴 ) = ∅ )